CRM CAMP in Nonlinear Analysis

October 20, 2020 from 10:00 to 11:00 (Montreal/EST time) Zoom meeting

Formally verified computer-assisted mathematical proofs

Seminar presented by 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

CRM CAMP in Nonlinear Analysis

Computer-Assisted Mathematical Proofs in Nonlinear Analysis

Seminar

Formally verified computer-assisted mathematical proofs