/-
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.
-/
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'$. The $n$-th term is the larger of $k$ and $k'$, so this says that the $n$-th term is odd. Conjecture 1 implies it.
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.
open 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$, the $n$-th term of A038552 is odd. The source states this as: the largest odd squarefree $k$ with $h(-k) = n$ is greater than the largest even one.
@[category research open, AMS 11]
theorem odd_of_isA038552 {n k : ℕ} (hn : Even n) (h : IsA038552 n k) : Odd k := n:ℕk:ℕhn:Even nh:IsA038552 n k⊢ Odd k
All goals completed! 🐙end OeisA38552