Imaginary quadratic fields of class number at most 2000
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.