Axiom Math says it has released roughly 43.1 million lines of Lean code formalizing the classification of finite simple groups. Mathematicians and engineers directed AI agents over 24 days and report resolving 34 significant departures from the published literature. The repository states that the proof contains no unfinished-proof placeholders and uses standard axioms. The announcement and code release can be confirmed, but they are not an independent rebuild of the full project or a comprehensive review that every formal definition faithfully captures the intended mathematics.