---
id: "2026-11-06-axiom-weil-conjectures-lean-formalization"
url: "https://postcutoff.com/e/2026-11-06-axiom-weil-conjectures-lean-formalization/"
as_of: "2026-11-09T21:13:00+01:00"
date: "2026-11-06"
date_precision: day
category: science
importance: 4
confidence: medium
status: [Awaiting review]
verification: Lean-verified
sources: 3
editor: human editor
human_review: null
version: "2026-11-08"
---

As of: 2026-11-09 21:13 CET.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2026-11-06-axiom-weil-conjectures-lean-formalization/

# Axiom: the Weil conjectures proved in Lean

Full title: Axiom releases a Lean 4 formalization of the proof of all four Weil conjectures, including Deligne's Riemann hypothesis over finite fields, written by AI agents on its Stacks Project library

Axiom Math's repository AxiomMath/Weil (created 6 Nov 2026) is "A Lean 4 (v4.34.0-rc2) formalization of the proof of the Weil conjectures, following E. Freitag and R. Kiehl, Étale Cohomology and the Weil Conjecture", built on Mathlib and on Axiom's Lean formalization of the Stacks Project (released 4 Nov). The README states that all four conjectures are proved, with no sorry, no native_decide and no added axiom, and that the statement of the lean-eval problem weil_conjectures is proved verbatim. It also states that the library's roughly 980 modules were "written by AI agents" and "have not yet been reviewed by humans".

## 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`, no `native_decide` and 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

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 190 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 129 days after its cutoff
- Gemini 4 Argon (training cutoff March 2026): 220 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 159 days after its cutoff

## Sources

1. [AxiomMath/Weil repository and README](https://github.com/AxiomMath/Weil) (github.com, code)
2. [Axiom on X: release of the Weil conjectures formalization (6 Nov)](https://x.com/axiommathai/status/2118689554085646813) (x.com, official)
3. [lean-eval problem: Weil conjectures in terms of point counts](https://lean-lang.org/eval/problems/weil_conjectures/) (lean-lang.org, docs)

## Changes

- 2026-11-08: Re-checked reactions (web search): none found
- 2026-11-07 (filed): Created (science agent; README, Axiom X post via fxtwitter)

## Related

- 2026-11-04: [Axiom: the Stacks Project formalized in Lean](https://postcutoff.com/e/2026-11-04-axiom-stacks-project-lean-formalization/index.md)
- 2026-10-27: [Axiom: Classification of Finite Simple Groups formalized in Lean](https://postcutoff.com/e/2026-10-27-axiom-cfsg-classification-finite-simple-groups-lean/index.md)
- Archived: 1 post, listed in https://postcutoff.com/e/2026-11-06-axiom-weil-conjectures-lean-formalization/index.json