All 16,453,493 imaginary quadratic fields with class number ≤ 2000 determined unconditionally, using OpenAI’s Siegel-zero proof made explicit in Lean with Claude Opus 5.5
Awaiting review
Importance: major (4 of 5)The takeaway
The first downstream theorem built on OpenAI’s claimed exclusion of Landau–Siegel zeros: the unconditional class-number table jumps from h ≤ 100 (Watkins, 2004) to h ≤ 2000, with the key bounds checked in Lean.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- Major (4 of 5)
- Last verified
- 16 October 2026
Your AI and this story
- GPT-6 Astra168 days after its cutoff
- Claude Opus 5.5107 days after its cutoff
- Gemini 4 Argon198 days after its cutoff
- Grok 4.7137 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 107 days before it.
Key facts
- Paper: ‘Imaginary quadratic fields of class number at most 2000’, Iwao Kimura, arXiv 2610.21511 [math.NT], 15 Oct 2026
- Theorem 1 (Lean): for χ primitive real of conductor q ≥ 3 and L(β, χ) = 0, (1 − β) log q ≥ 5811 · 10⁻⁷, and ≥ 1193/200000 once log q ≥ 35.0131
- Theorem 2: exactly 16,453,493 imaginary quadratic fields have class number ≤ 2000; largest |d| = 1,062,350,083 (h = 1978). For h ≤ 1000: 4,115,897 fields, largest |d| = 227,932,027 (h = 996). Matches the GRH-conditional data of Cremona–Sutherland and Holmin et al.
- Prior state: Watkins (2004) determined the fields with h ≤ 100; ‘To our knowledge, no unconditional list beyond h ≤ 100 was known’
- Status of the parts: the class-number bound (Theorem 10) is proved in Lean and checked by the Lean kernel, a replay and an independent kernel (nanoda), reusing OpenAI’s Lean formalization of the Siegel-zero manuscript, so it ‘does not depend on the correctness of the text of [SZ]’; the sieve computation for 6·2²⁸ ≤ |d| ≤ 1.65·10¹⁵ is argued in the paper but its program is not formally verified; small discriminants come from Mosunov–Jacobson tables
- AI statement (Section 8): ‘The following was done with Claude Opus 5.5 (Anthropic), used through Claude Code, under the author’s direction: (a) the explicit form of the argument of [SZ] … (b) the Lean files … (c) the sieve program … (d) the text of Sections 2 to 7 and of this section, written from the author’s outline’. ‘The author posed the problem and made the decisions that shaped the work’ and ‘worked through the proofs in the paper’
- Companion item the same day: Bryce Kerr, ‘A simpler proof that there are no Landau–Siegel zeros’, arXiv 2610.21099 (4 pages): replaces OpenAI’s interpolation-determinant analysis with the pigeonhole principle and a result of Masser; ‘ChatGPT assisted with the mathematical development and preparation of this paper’; Kerr thanks William Banks for a draft of his exposition
What happened
Siegel’s 1935 theorem says class numbers of imaginary quadratic fields grow, but its constant is ineffective because a real “Siegel zero” of a Dirichlet L-function could not be ruled out. That is why complete lists of fields with a given class number stopped at h ≤ 100 (Watkins, 2004), apart from GRH-conditional tables.
OpenAI’s internal model claimed on 1 Oct 2026 that Siegel zeros do not exist, with a Lean formalization but no explicit constant. William Banks wrote out an explicit version on 11 Oct. On 15 Oct Iwao Kimura posted arXiv 2610.215111, which proves its own explicit constant, (1 − β) log q ≥ 0.0005811, in Lean (reusing OpenAI’s formalization, not Banks’s text), derives an explicit class-number lower bound, and runs Watkins’s sieve up to |d| ≈ 1.65 · 10¹⁵. Result: exactly 16,453,493 imaginary quadratic fields have class number at most 2000, the largest discriminant in absolute value being 1,062,350,083.
The AI roles are listed in a dedicated section. OpenAI’s model produced the Siegel-zero manuscript and its Lean proof (“We took no part in them”). Claude Opus 5.5 in Claude Code worked out the explicit constants, wrote the Lean files and certificates, the sieve program and comparison scripts, and drafted Sections 2–7 “from the author’s outline”. The author made the design decisions, including basing the result on a formal proof rather than on OpenAI’s text, and checked the proofs and sources.
The same listing has Bryce Kerr’s four-page arXiv 2610.210992, “A simpler proof that there are no Landau–Siegel zeros”, which replaces OpenAI’s interpolation determinant with a pigeonhole argument and Masser’s theorem. “ChatGPT assisted with the mathematical development and preparation of this paper.”
No Hacker News thread or press coverage was found on 16 Oct (Algolia, web search); X was not searched.
Why it matters
This is the first concrete consequence drawn from OpenAI’s Siegel-zero claim, and it is built so that it does not trust the claim’s prose: the needed bounds are machine-checked. If the claim holds, effective results that number theory waited 90 years for become routine computations. Two independent rewrites (Banks, Kerr) and now a Lean-based application within two weeks also show how fast specialists are absorbing and checking the October release.
Caveats: unrefereed; the large sieve computation is not formally verified (it agrees with GRH-conditional tables where they overlap).
What is disputed or not yet verified
| Verification | Key theorems Lean-verified (two kernels); sieve computation not formally verified; unrefereed preprint; OpenAI’s manuscript itself unrefereed |
|---|
Sources
4 sources from 2 sites. Numbers match the chips in the text.
4 sources: 4 primary
Primary
- arXiv 2610.21511: Imaginary quadratic fields of class number at most 2000 (Kimura)arxiv.org, paper
- arXiv 2610.21099: A simpler proof that there are no Landau–Siegel zeros (Kerr)arxiv.org, paper
- arXiv 2610.15483: On the OpenAI proof that Landau-Siegel zeros do not exist (Banks)arxiv.org, paper
- OpenAI: Uniform exclusion of Landau–Siegel zeros (1 Oct manuscript)github.com, paper
Changes
- Filed from the PDFs of arXiv 2610.21511 and 2610.21099