A Machine-Checked Proof of the Odd Order Theorem
From MaRDI portal
Publication:5327343
DOI10.1007/978-3-642-39634-2_14zbMath1317.68211OpenAlexW1768814311WikidataQ56672736 ScholiaQ56672736MaRDI QIDQ5327343
Laurent Théry, Alexey Solovyev, Sidi Ould Biha, Jeremy Avigad, François Garillot, Ioana Paşca, Cyril Cohen, Assia Mahboubi, Russell O'Connor, Laurence Rideau, Enrico Tassi, Yves Bertot, Andrea Asperti, Georges Gonthier, Stéphane Le Roux
Publication date: 7 August 2013
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-39634-2_14
Finite solvable groups, theory of formations, Schunck classes, Fitting classes, (pi)-length, ranks (20D10) Mechanization of proofs and logical operations (03B35) Software, source code, etc. for problems pertaining to group theory (20-04)
Related Items
A FORMAL PROOF OF THE KEPLER CONJECTURE ⋮ A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem ⋮ A fully automatic theorem prover with human-style output ⋮ Deepalgebra -- an outline of a program ⋮ A Formalization of Properties of Continuous Functions on Closed Intervals ⋮ Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis ⋮ Deep Generation of Coq Lemma Names Using Elaborated Terms ⋮ Validating Mathematical Structures ⋮ Formalizing the Face Lattice of Polyhedra ⋮ From informal to formal proofs in Euclidean geometry ⋮ Mining the Archive of Formal Proofs ⋮ Towards the Formalization of Fractional Calculus in Higher-Order Logic ⋮ Formal verification of cP systems using Coq ⋮ Computational logic: its origins and applications ⋮ Certified Graph View Maintenance with Regular Datalog ⋮ Type theory and formalisation of mathematics ⋮ The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ Hammer for Coq: automation for dependent type theory ⋮ Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge ⋮ Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types ⋮ Formalizing Galois Theory ⋮ Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface ⋮ Computational Complexity Via Finite Types ⋮ Measure construction by extension in dependent type theory with application to integration ⋮ Computer-aided proof of Erdős discrepancy properties ⋮ Automating formalization by statistical and semantic parsing of mathematics ⋮ Formalization of the Lindemann-Weierstrass theorem ⋮ A formal proof in Coq of Lasalle's invariance principle ⋮ Certifying standard and stratified Datalog inference engines in SSReflect ⋮ A formalised theorem in the partition calculus ⋮ Formalising Mathematics in Simple Type Theory ⋮ What is the point of computers? A question for pure mathematicians ⋮ Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project ⋮ The formal verification of the ctm approach to forcing ⋮ Mathematizing as a virtuous practice: different narratives and their consequences for mathematics education and society ⋮ Reliability of mathematical inference ⋮ Mtac: A monad for typed tactic programming in Coq ⋮ A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading ⋮ A library for formalization of linear error-correcting codes ⋮ Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL ⋮ Recycling proof patterns in Coq: case studies ⋮ Proof Verification Technology and Elementary Physics ⋮ An introduction to mechanized reasoning ⋮ Mechanically certifying formula-based Noetherian induction reasoning ⋮ Incorporating quotation and evaluation into Church's type theory ⋮ Univalent categories and the Rezk completion ⋮ Homotopy limits in type theory ⋮ Foreword to the special focus on formal proofs for mathematics and computer science ⋮ An introduction to univalent foundations for mathematicians ⋮ Univalence as a principle of logic ⋮ The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem ⋮ Reshaping the metaphor of proof ⋮ A formalization of multi-tape Turing machines ⋮ Congruence Closure in Intensional Type Theory ⋮ MODULARITY IN MATHEMATICS ⋮ Towards the automatic mathematician ⋮ CATEGORY-BASED CO-GENERATION OF SEMINAL CONCEPTS AND RESULTS IN ALGEBRA AND NUMBER THEORY: CONTAINMENT-DIVISION AND GOLDBACH RINGS ⋮ Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem ⋮ Experiences from exporting major proof assistant libraries ⋮ Implementing type theory in higher order constraint logic programming ⋮ Classification of finite fields with applications ⋮ Mining State-Based Models from Proof Corpora ⋮ Towards Knowledge Management for HOL Light ⋮ Formalization of universal algebra in Agda ⋮ Proof Auditing Formalised Mathematics ⋮ Modelling algebraic structures and morphisms in ACL2 ⋮ Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
Uses Software
