Imaginary quadratic fields of class number at most 2000
Iwao Kimura
math.NT
Oct 15, 2026 · v1
TL;DR
Proves an explicit Landau–Siegel zero gap and an imaginary quadratic class-number lower bound in Lean 4 with Mathlib, checked by the Lean kernel and the independent nanoda kernel.
Abstract
We determine all imaginary quadratic fields with class number at most 2000, unconditionally: there are 16,453,493 of them, and the largest $|d_K|$ among them is 1,062,350,083. To our knowledge, such a list was previously known only for class number at most 100. We make explicit a recent argument, released by OpenAI and not refereed, that excludes Landau-Siegel zeros: every real zero $β$ of $L(s,χ)$, for a primitive real character $χ$ of conductor $q\ge3$, satisfies $(1-β)\log q\ge5.8\cdot10^{-4}$. An elementary lower bound for $L(1,χ)$ then shows that a field with class number at most 2000 has $|d_K|<1.61\cdot10^{15}$. The fields with $6\cdot2^{28}\le|d_K|\le1.65\cdot10^{15}$ are excluded by Watkins' sieve, and those below are read from the class group tables of Mosunov and Jacobson. As a consequence, the lists of Cremona and Sutherland of imaginary quadratic orders with class number at most 1000, and the counts of Holmin, Jones, Kurlberg, McLeman and Petersen for odd class numbers up to 1999, previously known under the generalized Riemann hypothesis, hold unconditionally. The two steps, the bound for $β$ and the bound for $|d_K|$, are proved in Lean, building on the existing formalization of that argument, and the proofs are checked by two independent kernels. The contributions of AI systems to this work are stated in the paper.
Problem
Unconditional lists of imaginary quadratic fields were known only for class number at most 100. Larger lists, such as those of Cremona–Sutherland for h ≤ 1000 and Holmin et al. for odd h, depend on GRH because no explicit bound excluding Landau–Siegel zeros was available.
Approach
The unrefereed OpenAI-produced argument [SZ] is made explicit: every real zero β of L(s,χ) satisfies (1-β)log q ≥ 5.8·10^-4. An elementary hyperbola-method lower bound for L(1,χ) then gives |d_K| < 1.61·10^15 when h ≤ 2000. Both theorems are proved in Lean 4 with Mathlib, reusing parts of the existing [SZ] formalization and certifying 314 numerical inequalities. Watkins' sieve excludes discriminants from 6·2^28 up to 1.65·10^15, and the Mosunov–Jacobson class group tables cover the range below.
Results
There are 16,453,493 imaginary quadratic fields with class number at most 2000, and the largest |d_K| is 1,062,350,083. This makes the GRH-conditional lists of Cremona–Sutherland and the counts of Holmin et al. unconditional. The Lean statements use only Mathlib definitions; the sieve program and the external tables are not formally verified.
| N | fields | largest d | h(-d) |
|---|
| 100 | 42,272 | 2,383,747 | 98 |
| 500 | 1,028,749 | 55,171,603 | 494 |
| 1000 | 4,115,897 | 227,932,027 | 996 |
| 2000 | 16,453,493 | 1,062,350,083 | 1978 |
Imaginary quadratic fields with h(-d) ≤ N