Chinese AI Startup Converts 20-Year Math Encyclopedia Into Verifiable Code

Axiom Math, an AI mathematics startup founded in 2025, has released a Lean formalization of the Stacks Project, a two-decade reference in algebra geometry created by Johan de Jong at Columbia University. The source project, built since 2005 and maintained through an open but centrally reviewed process, now spans 116 chapters, more than 7,600 pages and over 650 contributors, with each definition, lemma and theorem carrying a fixed four-character label and linked dependencies that let readers trace proofs. Axiom said its new code library, delivered Nov. 4 and based on the Lean community library Mathlib, contains about 15.75 million lines and covers all Stacks Project labels that can be formalized, while marking labels already in Mathlib or judged unsuitable for Lean. The release extends Axiom’s earlier Lean milestones, including formalization of the 246 prime gap result from Yitang Zhang’s breakthrough and the classification of finite simple groups, a proof originally requiring more than 100 mathematicians over decades. Unlike those one-off achievements, the Stacks formalization is structured as an evolving knowledge base. Axiom organized AI agents like an engineering team, assigning some to architecture, others to core definitions and others to individual proofs. It said the agents identified dozens of propositions needing local corrections and produced counterexamples where statements were invalid. The library is split into a manually verified core meeting Mathlib standards and an AI-generated frontier awaiting review. External contributors can claim frontier proofs, submit them for approval and move them into the core after human checks by Axiom’s four mathematician maintainers. The project will remain separate from the upstream Stacks repository for now, after de Jong asked in October that AI-generated comments and merge requests not be sent directly to the original site. The announcement also enters a broader debate over AI-driven formalization. Anthropic recently reported a large Lean formalization of Fermat’s Last Theorem, while Lean community figures warned that rapid code generation has limited value unless human mathematicians use and maintain the results. They argue formalized code should follow Mathlib conventions, undergo open review, avoid duplication and connect traceably to existing literature. For researchers, a verified, interconnected library could support proof search, paper review and incremental research; for AI systems, it could provide reliable mathematical building blocks that strengthen automated reasoning and generate further verified code. Human review remains the bottleneck. Kevin Buzzard, an Imperial College London mathematician active in Lean, has noted a backlog of unreviewed Mathlib contributions and said AI is not accepted as reviewer there, so even complete Stacks formalization may not enter Mathlib soon. Emerging projects such as Tau Ceti use AI-written code checked by other AI agents under human-designed rules, with about 3 million lines produced, but Lean’s kernel checks only logical validity, not whether a theorem faithfully represents the original mathematical meaning. Researchers still expect much of mathematics could be formalized in a reusable form within years, potentially exposing hidden gaps in conventional proofs and changing how mathematics is published, verified and extended.