Axiom has announced two related formal-mathematics releases: a Lean formalization of the Stacks Project on November 4, followed by the classical Weil conjectures on November 6. Together, the announcements emphasize building reusable infrastructure for mathematical reasoning rather than producing isolated proofs.
The Stacks announcement describes roughly 16 million lines of formal code linked to the permanent tags of the original reference work. Axiom says coordinated AI agents translated and integrated the material. The company credits the mathematicians whose decades of work produced the underlying mathematics and distinguishes its independent formalization from the actively maintained upstream Stacks Project.
From a library to another major theorem
The November 6 release says Axiom formalized the Weil conjectures using Mathlib and its Stacks development. These are classical results connecting geometry with counts of solutions to polynomial equations over finite fields. The news is their formalization in Lean, rather than the discovery of a new proof of the ordinary Riemann hypothesis.
Axiom presents the work as infrastructure future proofs can import. That reuse is central to the announcement: a formal library becomes more valuable when later developments can rely on its definitions and theorems without repeating the entire foundation.
What the repository says about coverage
The public Stacks repository describes a Lean 4 development built on Mathlib. It says tags with formalizable content are represented and that proofs contain neither sorry nor native_decide. It also identifies examples, exercises and remarks that remain tasks for contributors. That qualification is more precise than treating a large line count as proof that every sentence of a reference has an equivalent checked artifact.
This article has not independently built the full library. Claims about completeness and checking therefore remain attributed to Axiom and its documentation.
Why formal-library engineering matters
Our analysis is that the main engineering challenge is consistency across a highly connected body of work. Translating one theorem is different from choosing definitions that allow thousands of later statements to fit together. Stable references and dependency information help researchers inspect that structure.
Mechanical checking also leaves a human question: does the formal statement faithfully express the mathematics readers intend? Reviewers need to examine assumptions, definitions and the relationship to the source text. A valid proof of a mistranslated statement would not establish the original result.
The independent-project boundary is equally important. Mathematical communities maintain their own review standards and contribution processes. Publishing a separate formalization creates room for scrutiny and reuse without requiring upstream maintainers to absorb a flood of automated changes.
These releases offer a substantial case study in AI-assisted formalization. Their lasting value will depend on outside researchers being able to inspect, rebuild and use the library as a dependable foundation for further mathematics.