Formally verified computer-assisted mathematical proofs

Abstract: 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.

analysis of PDEsclassical analysis and ODEsdynamical systemsfunctional analysisnumerical analysis

Audience: researchers in the discipline

CRM CAMP (Computer-Assisted Mathematical Proofs) in Nonlinear Analysis

Series comments: To have access to the zoom details of the talks, please register at www.crm.math.ca/camp-nonlinear