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

zbMATH Open1540.68262MaRDI QIDQ6561744

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

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A classification of the maximal subgroups of the finite alternating and symmetric groups
• 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.
• Treatise on permutations and algebraic equations.
• The concept of primitivity in group theory and the second memoir of Galois
• Über die Einfachheit der speziellen projektiven Gruppen.
• Logicomix. An epic search for truth. Character design and drawings by Alecos Papadatos, color by Annie Di Donna
• Galois theory
• The Finite Simple Groups
• Finite Permutation Groups and Finite Simple Groups
• Liquid Tensor Experiment
• A FORMAL PROOF OF THE KEPLER CONJECTURE
• A Machine-Checked Proof of the Odd Order Theorem

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)