Axiom releases Lean formalization of Weil conjectures proof

Axiom has released a complete Lean formalization of Pierre Deligne's proof of the Weil conjectures, built directly on top of the company's previously released Stacks Project library. By leveraging existing abstractions for schemes, sheaves, and étale cohomology, Axiom's AI agents were able to complete the complex verification rapidly. The company argues this demonstrates how robust foundational libraries enable AI agents to scale formal mathematics and verified software engineering. Open article →