A formal proof is a proof that can be read and verified by computer, directly from the fundamental rules of logic and the foundational axioms of mathematics. The technology behind for mal proofs has been under development for decades and grew out of efforts in the early twentieth century to place mathematics on secure foundations. In recent years, this technology has made remarkable advances. Notably, a project led by Georges Gonthier has produced a complete for mal verification of the odd-order theorem of Feit and Thompson. This presentation will describe major recent developments in this field.
Séminaire Bourbaki, 66ème année (2013-2014), n°1086, juin 2014 PDF
By Thierry Coquand
By Ramon Flores
By Michael Kramer
By Angela Capel
By Anna Korba
![[1085] Théorie des types dépendants et axiome d'univalence](/media/cache/video_light/uploads/video/video-bcb9925c99f0fbef13d673ed5b4793e1.jpg)
![[1086] Developments in formal proofs](/media/cache/video_light/uploads/video/video-ce2a6dc8fc1735a3b803503c0f34563e.jpg)
![[1087] La conjecture de courbure $L^2$](/media/cache/video_light/uploads/video/video-7c75664be2af3aeb626632511afb25a1.jpg)
![[1088] Le problème de Kadison-Singer](/media/cache/video_light/uploads/video/video-b0a48a27494165d826a5083b86c9ab9b.jpg)
