Axiom: the Weil conjectures proved in Lean
Awaiting review
Importance: major (4 of 5)The takeaway
On 6 Nov 2026 Axiom Math published AxiomMath/Weil, a kernel-checked Lean 4 proof of rationality, the functional equation, the Riemann hypothesis (Deligne) and the Betti-number statement, following Freitag–Kiehl. About 980 modules were written by AI agents; the code has not been reviewed by humans.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- Major (4 of 5)
- Last verified
- 8 November 2026
Your AI and this story
- GPT-6 Astra190 days after its cutoff
- Claude Opus 5.5129 days after its cutoff
- Gemini 4 Argon220 days after its cutoff
- Grok 4.7159 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 129 days before it.
Key facts
- Reactions by 8 Nov: web search finds no mathematicians’ assessment or press coverage of the Weil release yet; Axiom’s earlier claims drew caution on the Lean Zulip
- Claim (README, verbatim): ‘All four Weil conjectures are proved: rationality, the functional equation, the Riemann hypothesis (Deligne’s theorem) and the Betti-number statement. Lean’s kernel checks every proof. There is no
sorry, nonative_decideand no added axiom.’ - Source followed: Freitag and Kiehl, ‘Étale Cohomology and the Weil Conjecture’ (Ergebnisse 13, Springer, 1988); Deligne’s theorem is obtained from the Stacks library’s LAdicSheaf.weightBound ‘proved in StacksFrontier along Laumon’s Fourier-transform route’; the Betti-number statement goes through Artin’s comparison theorem, also formalized
- Benchmark: the Mathlib-only statement of the lean-eval problem ‘weil_conjectures’ is proved verbatim (Weil/LeanEval/WeilConjectures.lean)
- AI role and review (README, verbatim): ‘[Weil] about 980 modules written by AI agents. Every proof is kernel-checked; the code has not yet been reviewed by humans.’ Which models were used is not stated
- Announcement: Axiom on X, 6 Nov 12:58 UTC, ‘Now, we release the Lean formalization of the proof of the renowned Weil conjectures (I-IV), one of which gives Riemann Hypothesis over finite fields’ (about 42k views, 265 likes on 7 Nov, fxtwitter); far less reach than the 4 Nov Stacks post (6.9M)
- Repository: github.com/AxiomMath/Weil, Apache 2.0, 13 stars on 6 Nov; no independent build or expert review reported as of 7 Nov
What happened
Two days after releasing a Lean formalization of the Stacks Project, Axiom Math published a Lean 4 library that proves the Weil conjectures, following Freitag and Kiehl’s textbook. Axiom presented it as the first major result built on the Stacks library (“The true test of a foundational library is what you can build on it”). The README lists the main theorems with their Lean statements and says the proofs use only the standard axioms.
The proof was not new mathematics: the conjectures were proved by Dwork, Grothendieck and Deligne (1960–1974). The claim is that the full proof, including Deligne’s theorem, is now machine-checked. According to the README, AI agents wrote the code and humans have not reviewed it. As of 7 Nov no one outside Axiom had reported rebuilding it or checking that the Lean statements match the classical ones.
Why it matters
Deligne’s proof rests on a large body of étale cohomology that formalization projects had treated as out of reach for years. If the build and statements hold up, this follows Axiom’s Classification of Finite Simple Groups formalization (27 Oct) as a second large body of classical mathematics checked by machine.
What is disputed or not yet verified
| Verification | Lean kernel-checked per the repository; not independently rebuilt or reviewed |
|---|
Sources
3 sources from 3 sites. Numbers match the chips in the text.
3 sources: 3 primary
Primary
- AxiomMath/Weil repository and READMEgithub.com, code
- Axiom on X: release of the Weil conjectures formalization (6 Nov)x.com, official
- lean-eval problem: Weil conjectures in terms of point countslean-lang.org, docs
Changes
- Re-checked reactions (web search): none found
- Filed (science agent; README, Axiom X post via fxtwitter)