Axiom Autoformalization Projects

Oct 2, 2026 · updated Oct 13, 2026

At Axiom, I’ve helped publish three autoformalization projects so far:

• BondalThomsen, a formalization of Exceptionality, strongness, and asymptotic rarity for the Bondal-Thomsen collection, preprint by Reginald Anderson
• DedekindZetaZeroFree (also on Palomar), a formalization of A quasi-Riemann hypothesis for Dedekind zeta functions, preprint by myself and Jesse Thorner on Hexagon
• A formalization of the Classification of Finite Simple Groups, the largest single-theorem Lean codebase ever written (43 million lines of code, produced in 24 days)

These projects contain complete Lean 4 formalizations generated by AxiomProver.