Computer-assisted proofs, proof assistants and visualization in dynamical systems
timetable:
Tue 18 Jun, 15:30 - 16:20, Aula Dini
<< Go back
The Lean theorem prover
speaker: Sébastien Gouëzel (CNRS and Université de Rennes)abstract: Interactive theorem provers are a kind of programming languages in which one explains proofs to a computer in a formal language, where the computer checks that the proof respects the rules of logic. I will present the Lean theorem prover, together with its mathematics library Mathlib. This library is advanced enough that one may start to formalize complicated statements in dynamics (and all other areas of mathematics!)
timetable:
Tue 18 Jun, 15:30 - 16:20, Aula Dini
<< Go back