Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore the mathematics of formal proofs and certified mathematics through this comprehensive lecture series from Institut Henri Poincaré's thematic trimester. Delve into the mature state of proof assistant technology and discover how non-trivial mathematical proofs can now be formalized and automatically verified within computers, as demonstrated by achievements like the four color theorem and ongoing work on the classification of finite groups and Kepler conjecture. Examine the rich mathematical foundations of formal proofs that emerged in the 1970s through the Curry-Howard correspondence, which reveals the fundamental connection between logical proofs and well-behaved programs. Investigate unexpected connections emerging between proof theory and diverse mathematical fields including homotopy theory, higher dimensional algebra, quantum topology, topos theory, functional analysis, and operator algebra. Learn about practical applications of proof assistants in certifying program properties, implementing certified compilers, and establishing security properties of protocols. Follow expert presentations from leading researchers including Georges Gonthier on digitizing group theory, Thomas Hales on formalizing the Kepler Conjecture proof, Xavier Leroy on proof assistants in computer science research, and Vladimir Voevodsky on univalent foundations. Study constructive semantics through Gérard Berry's lectures on electricity propagation in circuits, explore Jean-Yves Girard's philosophical investigations into analytical and epideictic reasoning, and examine Jean Louis Krivine's work on how Curry-Howard correspondence provides new models of ZF set theory. Discover cutting-edge developments in type theory through François Potier's presentations on Mezzo and Thorsten Altenkirch's exploration of cubical type theory syntax.
