The seminar takes place at Inria Bordeaux.
Proof assistants have two types of application: the construction of formal proofs of correctness for highly complex programs or algorithms (static compilers and analyzers, distributed algorithms, cryptographic protocols, etc. ), and formal proofs of theorems requiring the study of many complex cases (four-color theorems, Feit-Thompson theorem on the classification of groups, Kepler conjecture on the optimal ordering of spheres, etc.). These proofs are generally very large, which poses two major problems. Firstly, no human being can write down all the details; these are created by machine according to the strategies and fine-tuned indications provided by the user. Secondly, confidence in the correctness of a proof written with the help of a proof assistant comes from confidence in the proof-checking program present in the core of this assistant.
With the help of a few examples, we address the following questions:
The answer to these questions lies in two aspects: from a practical point of view, develop "proof patterns" similar to programming "design patterns"; understand the mathematical logic used by the proof assistant and validate the correctness of the proof verification algorithm.
