2014/08/24 by Thomas Hales, Thomas C. Hales, Hales, Thomas C. · 1 citation
Computer Science · Mathematics · #FOS: Computer and information sciences #FOS: Mathematics #Geometric and Algebraic Topology #Homotopy and Cohomology in Algebraic Topology #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #cs.LO #math.LO
paper · pdf · doi:10.48550/arxiv.1408.6474
Bourbaki seminar report 1086, June 2014
arxiv created 2014/08/24 · openalex publication_date 2014/08/24 · arxiv updated 2014/08/28 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
This report describes three particular technological advances in formal proofs. The HOL Light proof assistant will be used to illustrate the design of a highly reliable system. Today, proof assistants can verify large bodies of advanced mathematics; and as an example, we turn to the formal proof in Coq of the Feit-Thompson Odd Order theorem in group theory. Finally, we discuss advances in the automation of formal proofs, as implemented in proof assistants such as Mizar, Coq, Isabelle, and HOL Light.