A Machine-Checked Proof of the Odd Order Theorem

By Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, C. Cohen, François Garillot, Stéphane Le Roux, A. Mahboubi, Russell O'Connor, S. Biha and 5 more. International Conference on Interactive Theorem Proving, 2013

396 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics

View Paper: https://www.semanticscholar.org/paper/6770570a45fe0fa38000e2465f8338604da7f312

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

Citations in the corpus

Learning to Prove Theorems via Interacting with Proof Assistants (2019, methodology): “GamePad includes a tool for interacting with Coq as well as data collected from the proof of the Feit Thompson theorem (Gonthier et al., 2013).”
The simplicial model of Univalent Foundations (after Voevodsky) (2012, positive): “…on the Calculus of Inductive Constructions (a closely related dependent type theory), which has shown itself feasible for large-scale formal veriﬁcation of mathematics, with developments including formal proofs of the Four-Colour Theorem [Gon08] and the Feit-Thompson (Odd Order) Theorem [GAA + 13].”
Premise Selection for Theorem Proving by Deep Graph Embedding (2017, positive): “This limitation gave rise to the development of interactive theorem proving [11] such as Coq [14] and Isabelle [15], which combines humans and machines in theorem proving and has led to impressive achievements such as the proof of the Kepler conjecture [16] and the formal proof of the Feit-Thompson ”
Autoformalization with Large Language Models (2022, methodology): “Formal Mathematics A few important and complex results of mathematics and computer science have been formalized manually using interactive theorem provers, such as the four color theorem [16], the Kepler conjecture [20], the odd-order theorem [17] and the verification of a microkernel [27].”
Developing Bug-Free Machine Learning Systems With Formal Mathematics (2017, background): “…Chli-pala, 2013; Chen et al., 2015), which has aimed to prove properties of computer programs, and formal mathematics (Rudnicki, 1992; Gonthier, 2008; Gonthier et al., 2013; Hales et al., 2015), which has aimed to formally represent and generate machine-checkable proofs of mathematical theorems.”
Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs (2020, background): “Over the last decade, nontrivial mathematical theorems [16, 18, 19], security protocols [14, 40], and industry-scale software systems [27, 32] have been mechanically checked, highlighting numerous issues and bugs.”
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers (2022, background): “Hence, projects such as the formalisation of complicated mathematical results [Gonthier et al., 2008, Avigad et al., 2007, Gonthier et al., 2013, Scholze, 2021] and operating system kernel veriﬁcation [Klein et al., 2009] are done in interactive theorem provers, often based on higher-order logic or…”