Developments in formal proofs

MaRDI QIDQ2967791zbMATH OpenFDO

Authors Thomas C. Hales

Publication date 2 March 2017

Full work available at URL https://arxiv.org/abs/1408.6474

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Mechanization of proofs and logical operations (03B35)

Abstract: 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.

Recommendations

• Formal proof -- theory and practice
• Autarkic computations in formal proofs
• Mining the Archive of Formal Proofs
• Engineering mathematics: the odd order theorem proof
• Foreword to the special focus on formal proofs for mathematics and computer science

Cited in

(9)

• Engineering mathematics: the odd order theorem proof
• Proof verification technology and elementary physics
• A formal proof of the Kepler conjecture
• Formal proof -- theory and practice
• A machine-checked proof of the odd order theorem
• scientific article; zbMATH DE number 5269066 (Why is no real title available?)
• Automated Reasoning with Analytic Tableaux and Related Methods
• Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project
• Mathematics and the formal turn

Describes a project that uses

Uses Software

• Mizar
• HOL Light
• Isabelle
• Coq

This page was built for publication: Developments in formal proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2967791)