An experiment of a formal proof of an intermediate-level theorem in algebra

MaRDI QIDQ6561744zbMATH OpenFDO

Authors Antoine Chambert-Loir

Publication date 25 June 2024

Published in La Gaceta de la Real Sociedad Matemática Española (Search for Journal in Brave)

Mathematics Subject Classification ID

Multiply transitive finite groups (20B20) Subgroups of symmetric groups (20B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A classification of the maximal subgroups of the finite alternating and symmetric groups
• A formal proof of the Kepler conjecture
• A machine-checked proof of the odd order theorem
• Finite Permutation Groups and Finite Simple Groups
• Formal proof - the four color theorem
• Galois theory
• scientific article; zbMATH DE number 3887879 (Why is no real title available?)
• scientific article; zbMATH DE number 42070 (Why is no real title available?)
• Liquid tensor experiment
• Logicomix. An epic search for truth. Character design and drawings by Alecos Papadatos, color by Annie Di Donna
• On some maximal subgroups of the classical groups
• Principia mathematica. Vol 2, 3. 2. ed.
• Sur la limite de transitivité des groupes non alternés.
• The concept of primitivity in group theory and the second memoir of Galois
• The Finite Simple Groups
• Treatise on permutations and algebraic equations.
• Über die Einfachheit der speziellen projektiven Gruppen.

This page was built for publication: An experiment of a formal proof of an intermediate-level theorem in algebra

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