Speaker: Jaime Gaspar (Centro de Matemática e Aplicações - CMA, FCT, UNL).

Abstract: Proof assistants are computer programs that help mathematicians to prove theorems and to formally verify the correctness of proofs. Proof assistants are nowadays one of the more exciting areas in the intersection of mathematical logic and computer science. For example, one particularly exciting achievement is the formal verification of the proof of the four colour theorem using the proof assistant Coq. In this talk we give a very elementary introduction to Coq by means of a very simple example: the proofs of the theorems (1) if ≤ is a non-strict partial order, then < defined by x < y ↔ x ≤ y ∧ x ≠ y is a strict partial order; (2) if < is a strict partial order, then ≤ defined by x ≤ y ↔ x < y ∨ x = y is a non-strict partial order. Then we end by discussing what is achieved with this kind of formal verification. We keep this talk very short, simple and sweet.

Zoom Meeting | Meeting ID: 890 8479 3299 | Password: 409604