CRM CAMP in Nonlinear Analysis

Preuves mathématiques assistées par ordinateur en analyse non linéaire

20 octobre 2020 de 10 h 00 à 11 h 00 (heure de Montréal/HNE) Réunion Zoom

Formally verified computer-assisted mathematical proofs

Séminaire par Assia Mahboubi (Inria, France & VU Amsterdam, Netherlands)

Proof assistants are pieces of software designed for defining formally mathematical objects, statement and proofs. In particular, such a formalization reduces the verification of proofs to a purely mechanical well-formedness check. Since the early 70s, proof assistants have been extensively used for applications in program verification, notably for security-related issues. They have also been used to verify landmark results in mathematics, including theorems with a computational proof, like the Four Colour Theorem (Appel and Haken, 1977) or Hales and Ferguson's proof of the Kepler conjecture (2005). This talk will discuss what are formalized mathematics and formal proofs, and sketch the architecture of modern proof assistants. It will also showcase a few applications in formally verified rigorous computation.

The slides of the talk are available here