AI Proved What?

AX07 (outside OpenAI’s math catalogue), November 2026

The Weil conjectures, all in Lean?

Axiom Math says all four Weil conjectures are proved in Lean. Its README says the code was written by AI agents and has not yet been reviewed by humans, and the decisive step comes from the unreviewed tier of its Stacks Project library.

Play AX07: the Weil conjectures in Lean. A circle with two yellow points (the eigenvalues of our example curve), and a three-block tower with an orange piece in the middle block for the imported weight estimate.

6:27. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The question
  2. 2:07The claim
  3. 3:41What it rests on
  4. 5:03Where it stands

The claim, in plain words

This is AX07. Take the curve y² = x³ + x + 1, and let x and y run over the integers modulo 5. Eight pairs fit, and with one point at infinity that makes nine points. Over the field with 25 elements the same equation has 27 points, and over the field with 125 elements, 108. In 1949, André Weil proposed that such counts, for any smooth projective variety over a finite field, follow a strict pattern. Put all of them into one generating function, the zeta function. For this curve it collapses to a fraction: (1 + 3T + 5T²)/((1 − T)(1 − 5T)).

The numerator hides two numbers, α and β, with α + β = −3 and αβ = 5. Both have absolute value exactly √5: they sit on one circle. That is the Riemann hypothesis for curves over finite fields, and it bounds the count. Nine lies within 2√5 of 5 + 1. For a curve of genus g, the bound is 2g√q. Hasse proved it for elliptic curves in the 1930s, and Weil for all smooth projective curves in the 1940s. The curve’s numbers are our own computation.

Weil’s conjectures have four parts. The zeta function is rational. It satisfies a functional equation. Its zeros obey a Riemann hypothesis. And the degrees of its factors are the Betti numbers of a matching complex variety, counts of its features in each dimension. Dwork proved rationality first, published in 1960. Grothendieck, with Artin and Verdier, built étale cohomology, which explained rationality, the functional equation and the Betti numbers. Deligne’s proof of the Riemann hypothesis was published in 1974, and a broader theory of weights, Weil II, in 1980. So this is known mathematics. The new question is whether a computer can check all of it.

On November 6, 2026, Axiom Math published a blog post and a public Lean repository. The README says all four Weil conjectures are proved, with no sorry, no native_decide and no added axiom. It follows the 1988 book by Freitag and Kiehl, and builds on Mathlib and on Axiom’s Stacks Project library from AX06. The library has about 980 modules; by our count, about 213,000 lines. Rationality is stated for any scheme of finite type, the Riemann hypothesis for smooth proper varieties, and the Betti numbers under good reduction from the complex numbers. This formalizes known mathematics. It is not a new theorem, and by the post’s own account it does not reproduce Deligne’s 1974 proof line by line.

What it doesn’t claim

One strength stands out. In August, LeanEval, an outside benchmark of formalization problems, added a statement of the Weil conjectures submitted by Junyan Xu, written with Mathlib definitions only. Axiom’s README says the repository proves that statement word for word, and our own text comparison agrees the statement matches. So a reader can check the target without first trusting Axiom’s own definitions. Two limits. The benchmark statement leaves out the Betti numbers. And we found no comparator run, the tool that mechanically confirms a proof proves exactly the benchmark’s theorem with only allowed axioms, and no entry for it among the benchmark’s results.

No new theorem: this is known mathematics, formalized, and by Axiom’s own account not Deligne’s 1974 proof line by line. The post also says the Ramanujan bound is not part of this formalization.

Where it stands

Released by Axiom
Blog post and repository, November 6, 2026: three commits by Tony Yue Yu within 22 minutes (November 6 UTC), the last 27cdb20. The post says the repository’s scope and review status were checked on November 5.
Human review
Not yet. The README: about 980 modules “written by AI agents”; “the code has not yet been reviewed by humans”. The decisive weight estimate comes from StacksFrontier, which Axiom’s metadata says “has not yet had human review” (see AX06). The blog post lists nine people and does not mention AI.
Independent check
None found as of November 6, 2026: no GitHub Actions runs, no comparator file, no comparator run or results entry for the LeanEval statement, no outside build, review or expert reaction.
Peer reviewed
No (there is no paper).
Lean library, by Axiom
Lean v4.34.0-rc2, Mathlib 16edf57, on Axiom’s Stacks library pinned at 012108f (Axiom’s Stacks repository moved to Lean v4.35.0 on November 6); no sorry, no native_decide and no added axiom, per the README (our text grep of the 980 files agrees). Not built or run by us.

Last checked November 6, 2026. Where it stands. The repository holds three commits, all by Tony Yue Yu, made within 22 minutes on November 6, universal time. There are no continuous-integration runs and no comparator file. It is built on Lean v4.34.0-rc2, and on the pinned Stacks commit, while Axiom’s Stacks repository moved to Lean v4.35.0 the same day. The README says the first build takes a long time and a lot of memory. We found no independent build or review of it. A separate group’s Lean formalization of the Weil conjectures, mostly written by AI agents too, is also public; it says a full comparator run has not completed yet. Nothing here is peer reviewed, and we did not build or run either.

This is outside OpenAI’s math catalogue. It is the sequel to AX06, Axiom’s Stacks Project formalization, and pairs with AX01, its Lean proof of the classification of finite simple groups. If it holds, all four Weil conjectures are now Lean theorems that later proofs can use, and three of them in a form fixed by an outside benchmark. But the decisive estimate sits in Axiom’s AI-written Stacks tier, and neither the Weil code nor that Stacks tier, Axiom says, has yet been reviewed by people. See AX06 and AX01.

What it rests on

  1. The dependency. What it rests on. Picture a tower. At the bottom, Mathlib. Above it, Axiom’s Stacks library, pinned to one exact commit: the November 5 build fix we noted after AX06. On top, the Weil library. The hardest step, Deligne’s weight estimate, is not proved in the Weil repository. It is imported, as the theorem weightBound, for Stacks tag 03VH. On the Stacks Project’s own page, that tag’s proof is a citation of Deligne’s paper. Axiom’s post puts it this way: in Lean, citing that tag is not enough. So Axiom proved it in StacksFrontier, along Laumon’s later Fourier-transform route. And StacksFrontier is the tier that, by Axiom’s own metadata, has not yet had human review.
  2. Who wrote it. Who wrote it? The blog post lists nine people, led by Tony Yue Yu, with Ken Ono among the contributors. It never mentions AI. The README says the library’s roughly 980 modules were written by AI agents. Every proof is kernel-checked, it says, but the code has not yet been reviewed by humans. The two documents describe the same work differently, and only the README states the review status. About 1,800 tags in the code link declarations to items of the book, by our count, which gives a reader a map from book to Lean.

The numbers in the video

  • Ours: the curve y² = x³ + x + 1 has 9, 27 and 108 points over F_5, F_25 and F_125 (brute force); its zeta function is (1 + 3T + 5T²)/((1 − T)(1 − 5T)); α, β = (−3 ± i√11)/2, so |α| = |β| = √5, and |9 − 6| = 3 ≤ 2√5 ≈ 4.47.
  • Ours: the repository at 27cdb20 has 980 Lean files, 213,159 lines and 1,838 @[weil] tags; our text grep finds no sorry, admit, native_decide or axiom declaration. The Weil library uses the Stacks theorem LAdicSheaf.weightBound and does not reprove it.
  • The LeanEval problem weil_conjectures (submitted by Junyan Xu, added 2026-08-03) and Axiom’s theorem have the same statement, word for word up to spacing (our comparison). Its docstring says it does not include the Betti numbers.
  • Stacks tag 03VH (Theorem 64.27.4, Deligne, Weil II): the Stacks Project’s proof is a citation of Weil II; Axiom’s Lean proof is in StacksFrontier, in WeilIIWeightBound.lean at the pinned commit 012108f.
  • From Axiom’s post: Weil 1949; Hasse in the 1930s for elliptic curves; Weil in the 1940s for curves; Dwork, published 1960; Deligne, 1974 (Weil I) and 1980 (Weil II); Freitag and Kiehl, 1988.

Read the source

AI Proved What? is independent and not affiliated with Axiom Math, OpenAI, LeanEval or the Stacks Project.

Transcript

Read the full script

0:00The question

This is AX07. Take the curve y² = x³ + x + 1, and let x and y run over the integers modulo 5. Eight pairs fit, and with one point at infinity that makes nine points. Over the field with 25 elements the same equation has 27 points, and over the field with 125 elements, 108. In 1949, André Weil proposed that such counts, for any smooth projective variety over a finite field, follow a strict pattern. Put all of them into one generating function, the zeta function. For this curve it collapses to a fraction: (1 + 3T + 5T²)/((1 − T)(1 − 5T)). The numerator hides two numbers, α and β, with α + β = −3 and αβ = 5. Both have absolute value exactly √5: they sit on one circle. That is the Riemann hypothesis for curves over finite fields, and it bounds the count. Nine lies within 2√5 of 5 + 1. For a curve of genus g, the bound is 2g√q. Hasse proved it for elliptic curves in the 1930s, and Weil for all smooth projective curves in the 1940s. The curve’s numbers are our own computation. Weil’s conjectures have four parts. The zeta function is rational. It satisfies a functional equation. Its zeros obey a Riemann hypothesis. And the degrees of its factors are the Betti numbers of a matching complex variety, counts of its features in each dimension. Dwork proved rationality first, published in 1960. Grothendieck, with Artin and Verdier, built étale cohomology, which explained rationality, the functional equation and the Betti numbers. Deligne’s proof of the Riemann hypothesis was published in 1974, and a broader theory of weights, Weil II, in 1980. So this is known mathematics. The new question is whether a computer can check all of it.

2:07The claim

On November 6, 2026, Axiom Math published a blog post and a public Lean repository. The README says all four Weil conjectures are proved, with no sorry, no native_decide and no added axiom. It follows the 1988 book by Freitag and Kiehl, and builds on Mathlib and on Axiom’s Stacks Project library from AX06. The library has about 980 modules; by our count, about 213,000 lines. Rationality is stated for any scheme of finite type, the Riemann hypothesis for smooth proper varieties, and the Betti numbers under good reduction from the complex numbers. This formalizes known mathematics. It is not a new theorem, and by the post’s own account it does not reproduce Deligne’s 1974 proof line by line. One strength stands out. In August, LeanEval, an outside benchmark of formalization problems, added a statement of the Weil conjectures submitted by Junyan Xu, written with Mathlib definitions only. Axiom’s README says the repository proves that statement word for word, and our own text comparison agrees the statement matches. So a reader can check the target without first trusting Axiom’s own definitions. Two limits. The benchmark statement leaves out the Betti numbers. And we found no comparator run, the tool that mechanically confirms a proof proves exactly the benchmark’s theorem with only allowed axioms, and no entry for it among the benchmark’s results.

3:41What it rests on

What it rests on. Picture a tower. At the bottom, Mathlib. Above it, Axiom’s Stacks library, pinned to one exact commit: the November 5 build fix we noted after AX06. On top, the Weil library. The hardest step, Deligne’s weight estimate, is not proved in the Weil repository. It is imported, as the theorem weightBound, for Stacks tag 03VH. On the Stacks Project’s own page, that tag’s proof is a citation of Deligne’s paper. Axiom’s post puts it this way: in Lean, citing that tag is not enough. So Axiom proved it in StacksFrontier, along Laumon’s later Fourier-transform route. And StacksFrontier is the tier that, by Axiom’s own metadata, has not yet had human review. Who wrote it? The blog post lists nine people, led by Tony Yue Yu, with Ken Ono among the contributors. It never mentions AI. The README says the library’s roughly 980 modules were written by AI agents. Every proof is kernel-checked, it says, but the code has not yet been reviewed by humans. The two documents describe the same work differently, and only the README states the review status. About 1,800 tags in the code link declarations to items of the book, by our count, which gives a reader a map from book to Lean.

5:03Where it stands

Where it stands. The repository holds three commits, all by Tony Yue Yu, made within 22 minutes on November 6, universal time. There are no continuous-integration runs and no comparator file. It is built on Lean v4.34.0-rc2, and on the pinned Stacks commit, while Axiom’s Stacks repository moved to Lean v4.35.0 the same day. The README says the first build takes a long time and a lot of memory. We found no independent build or review of it. A separate group’s Lean formalization of the Weil conjectures, mostly written by AI agents too, is also public; it says a full comparator run has not completed yet. Nothing here is peer reviewed, and we did not build or run either. This is outside OpenAI’s math catalogue. It is the sequel to AX06, Axiom’s Stacks Project formalization, and pairs with AX01, its Lean proof of the classification of finite simple groups. If it holds, all four Weil conjectures are now Lean theorems that later proofs can use, and three of them in a form fixed by an outside benchmark. But the decisive estimate sits in Axiom’s AI-written Stacks tier, and neither the Weil code nor that Stacks tier, Axiom says, has yet been reviewed by people.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.