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

zbMATH Open1540.68262MaRDI QIDQ6561744FDOQ6561744

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

• Title not available (Why is that?)
• The Finite Simple Groups
• Title not available (Why is that?)
• Finite Permutation Groups and Finite Simple Groups
• A classification of the maximal subgroups of the finite alternating and symmetric groups
• Formal proof - the four color theorem
• Galois theory
• Logicomix. An epic search for truth. Character design and drawings by Alecos Papadatos, color by Annie Di Donna
• A Machine-Checked Proof of the Odd Order Theorem
• On some maximal subgroups of the classical groups
• The concept of primitivity in group theory and the second memoir of Galois
• A FORMAL PROOF OF THE KEPLER CONJECTURE
• Principia mathematica. Vol 2, 3. 2. ed.
• Sur la limite de transitivité des groupes non alternés.
• Treatise on permutations and algebraic equations.
• Über die Einfachheit der speziellen projektiven Gruppen.
• Liquid Tensor Experiment

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)