/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module
public import FormalConjecturesUtilConjectures associated with A038552
A038552 lists the largest squarefree number $k$ such that the imaginary quadratic field $\mathbb{Q}(\sqrt{-k})$ has class number $n$.
The conjectures state that:
All terms are congruent to $19 \pmod{24}$.
This is also the largest absolute value of negative fundamental discriminant $d$ for class number $n$.
For even $n$, if $k$ is the largest odd number with $h(-k) = n$ and $k'$ is the largest even number with $h(-k') = n$, then $k > k'$. Here $h(D)$ is the class number of the quadratic field with discriminant $D$, so $k$ and $k'$ are absolute values of negative fundamental discriminants, not radicands. The source states conjecture 2 in this form.
The squarefree condition in the definition is needed for the maximum to exist, since $\mathbb{Q}(\sqrt{-k}) = \mathbb{Q}(\sqrt{-4k})$.
Conjecture 2 is not a restatement of the definition. Both maxima range over the same imaginary quadratic fields, but they maximize different integers attached to those fields. A038552 uses the squarefree radicand $k$, whereas the discriminant of $\mathbb{Q}(\sqrt{-k})$ is $-k$ for $k \equiv 3 \pmod 4$ and $-4k$ otherwise. The map $k \mapsto |d|$ is not monotone: it sends $2$ to $8$ and $3$ to $3$. So conjecture 2 says that the largest term $k$ satisfies $k \equiv 3 \pmod 4$, and that $4k' \le k$ for every $k' \equiv 1, 2 \pmod 4$ with class number $n$.
References:
[Sta67] Stark, Harold M. "A complete determination of the complex quadratic fields of class-number one." Michigan Mathematical Journal 14.1 (1967): 1-27.
@[expose] public sectionopen NumberField Polynomialnamespace OeisA38552The class number of the imaginary quadratic field $\mathbb{Q}(\sqrt{-k})$ equals $n$.
def HasClassNumber (k n : ℕ) : Prop :=
∃ (h : Irreducible (X ^ 2 + C (k : ℚ))),
haveI := Fact.mk h
NumberField.classNumber (AdjoinRoot (X ^ 2 + C (k : ℚ))) = n$k$ is maximal among squarefree numbers such that $\mathbb{Q}(\sqrt{-k})$ has class number $n$. This defines the $n$-th term of A038552.
def IsA038552 (n k : ℕ) : Prop :=
MaximalFor (fun m => Squarefree m ∧ HasClassNumber m n) id kThe class number of the quadratic field with discriminant $d$.
noncomputable def classNumberOfDiscriminant (d : ℤ) : ℕ :=
haveI := Classical.dec (Irreducible (X ^ 2 - C (d : ℚ)))
if h : Irreducible (X ^ 2 - C (d : ℚ)) then
haveI := Fact.mk h
NumberField.classNumber (AdjoinRoot (X ^ 2 - C (d : ℚ)))
else 0$|d|$ is the largest absolute value among negative fundamental discriminants with class number $n$.
def IsLargestNegFundDiscrForClassNumber {n : ℕ} (absD : ℕ) : Prop :=
IsGreatest {m : ℕ | IsFundamentalDiscr (-m : ℤ) ∧ classNumberOfDiscriminant (-m : ℤ) = n}
absDThe Stark-Heegner theorem [Sta67] implies that the squarefree $k > 0$ such that $\mathbb{Q}(\sqrt{-k})$ has class number $1$ are exactly ${1, 2, 3, 7, 11, 19, 43, 67, 163}$.
@[category research solved, AMS 11]
theorem starkHeegner_classNumberOne :
{k : ℕ | Squarefree k ∧ HasClassNumber k 1} = {1, 2, 3, 7, 11, 19, 43, 67, 163} := ⊢ {k | Squarefree k ∧ HasClassNumber k 1} = {1, 2, 3, 7, 11, 19, 43, 67, 163}
All goals completed! 🐙$\mathbb{Q}(\sqrt{-163})$ has class number $1$.
@[category API, AMS 11]
theorem hasClassNumber_163_1 : HasClassNumber 163 1 := ⊢ HasClassNumber 163 1
h:{k | Squarefree k ∧ HasClassNumber k 1} = {1, 2, 3, 7, 11, 19, 43, 67, 163}⊢ HasClassNumber 163 1
h:∀ (x : ℕ),
Squarefree x ∧ HasClassNumber x 1 ↔ x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 7 ∨ x = 11 ∨ x = 19 ∨ x = 43 ∨ x = 67 ∨ x = 163⊢ HasClassNumber 163 1
exact ((h 163).mpr (h:∀ (x : ℕ),
Squarefree x ∧ HasClassNumber x 1 ↔ x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 7 ∨ x = 11 ∨ x = 19 ∨ x = 43 ∨ x = 67 ∨ x = 163⊢ 163 = 1 ∨ 163 = 2 ∨ 163 = 3 ∨ 163 = 7 ∨ 163 = 11 ∨ 163 = 19 ∨ 163 = 43 ∨ 163 = 67 ∨ 163 = 163 All goals completed! 🐙)).2$163$ is the largest squarefree $k$ with class number $1$.
@[category test, AMS 11]
theorem isA038552_1_163 : IsA038552 1 163 := ⊢ IsA038552 1 163
refine ⟨⟨(⊢ Nat.Prime 163 All goals completed! 🐙 : Nat.Prime 163).squarefree, hasClassNumber_163_1⟩, ?_⟩
m:ℕhm_sq:Squarefree mhm_class:HasClassNumber m 1hle:163 ≤ m⊢ id m ≤ id 163
m:ℕhm_sq:Squarefree mhm_class:HasClassNumber m 1hle:163 ≤ mhm_in:m ∈ {1, 2, 3, 7, 11, 19, 43, 67, 163}⊢ id m ≤ id 163
m:ℕhm_sq:Squarefree mhm_class:HasClassNumber m 1hle:163 ≤ mhm_in:m = 1 ∨ m = 2 ∨ m = 3 ∨ m = 7 ∨ m = 11 ∨ m = 19 ∨ m = 43 ∨ m = 67 ∨ m = 163⊢ m ≤ 163
All goals completed! 🐙All terms of A038552 are congruent to $19 \pmod{24}$.
@[category research open, AMS 11]
theorem mod_24_of_isA038552 {n k : ℕ} (h : IsA038552 n k) : k % 24 = 19 := n:ℕk:ℕh:IsA038552 n k⊢ k % 24 = 19
All goals completed! 🐙A038552 also gives the largest absolute value of negative fundamental discriminant for each class number.
@[category research open, AMS 11]
theorem isA038552_eq_largestNegFundDisc {n k : ℕ} (h : IsA038552 n k) :
IsLargestNegFundDiscrForClassNumber (n := n) k := n:ℕk:ℕh:IsA038552 n k⊢ IsLargestNegFundDiscrForClassNumber k
All goals completed! 🐙For even class number $n$, let $k$ be the largest odd number such that the quadratic field with discriminant $-k$ has class number $n$, and let $k'$ be the largest even such number, when they exist. Then $k > k'$.
@[category research open, AMS 11]
theorem largestEven_lt_largestOdd_negFundDisc {n k k' : ℕ} (hn : Even n)
(hk : IsGreatest {m : ℕ | Odd m ∧ IsFundamentalDiscr (-m : ℤ) ∧
classNumberOfDiscriminant (-m : ℤ) = n} k)
(hk' : IsGreatest {m : ℕ | Even m ∧ IsFundamentalDiscr (-m : ℤ) ∧
classNumberOfDiscriminant (-m : ℤ) = n} k') : k' < k := n:ℕk:ℕk':ℕhn:Even nhk:IsGreatest {m | Odd m ∧ IsFundamentalDiscr (-↑m) ∧ classNumberOfDiscriminant (-↑m) = n} khk':IsGreatest {m | Even m ∧ IsFundamentalDiscr (-↑m) ∧ classNumberOfDiscriminant (-↑m) = n} k'⊢ k' < k
All goals completed! 🐙end OeisA38552