Axiom says it has formalised Pierre Deligne’s proof of the Weil conjectures in Lean, building on its earlier Stacks Project library. The company’s claim is a striking example of AI agents being used to help produce machine-checkable mathematics, not simply to suggest a proof.
Watch Desk analysis
What happened
Axiom says the formalisation uses existing Lean abstractions for schemes, sheaves and étale cohomology from its Stacks Project work. The company says its AI agents completed the complex verification rapidly, though its announcement does not provide further detail here on the agents’ workflow or the amount of human involvement.
The new work is distinct from the earlier Stacks Project formalisation: it applies that library to Deligne’s proof of the Weil conjectures. Axiom presents the result as a demonstration of how foundational libraries can help agents scale formal mathematics and verified software engineering.
Why it matters
Lean checks proofs against explicit rules. A formalisation therefore offers something more useful than a confident-looking explanation: a proof encoded in a form that the system can check, and that other researchers may be able to inspect and build on.
The practical idea is cumulative. Instead of asking an AI system to tackle a difficult proof from scratch, researchers can give it a substantial library of formalised concepts to work with. Whether that approach scales depends on the quality and usability of the resulting work, not just how quickly it was produced.
Our read
This is a substantial and unusually concrete use of AI in mathematics. The promise is not that agents have replaced mathematicians, but that well-built formal libraries may let them contribute to work that is verifiable and reusable. Axiom’s account makes an important claim; the next step is for mathematicians to test how useful the formalisation is in practice.
What to watch
- Whether researchers use or extend the Lean formalisation.
- How Axiom documents the agents’ process and human contribution.
- Whether the approach transfers to other difficult proofs.
Discussion spark: Should AI-assisted formal proofs be judged mainly by machine-checkability, or should researchers also expect a clear account of the agents’ work and human contribution?
Sources and evidence
- The Weil Conjectures, Formalized in Lean | Axiom (6 November 2026, 00:00 UTC)
Watch Desk is operated by WittyWires as an independent cross-cutting AI news tracker. It does not speak for the organisations or people it covers.