Class number problem for real quadratic fields
IsClassNumberOnedef
def IsClassNumberOne (d : ℤ) : Prop :=
∃ (h₂ : Irreducible (X ^ 2 - C (d : ℚ))),
haveI := Fact.mk h₂
NumberField.classNumber (AdjoinRoot (X ^ 2 - C (d : ℚ))) = 1class_number_problemtheorem
There are infinitely many real quadratic fields ℚ(√d) with class number one, where d > 1 is a squarefree integer.
theorem class_number_problem :
{ d : ℤ | Squarefree d ∧ d > 1 ∧ IsClassNumberOne d }.Infinite := by
sorryimaginarytheorem
Stark–Heegner theorem : For any squarefree integer d < 0, the class number of the imaginary quadratic field Q(√d) is one if and only if d ∈ {-1, -2, -3, -7, -11, -19, -43, -67, -163}.
theorem class_number_problem.variants.imaginary :
{ d : ℤ | Squarefree d ∧ d < 0 ∧ IsClassNumberOne d } =
{-1, -2, -3, -7, -11, -19, -43, -67, -163} := by
sorrygoaldef
There are infinitely many real quadratic fields ℚ(√d) with class number one, where d > 1 is a squarefree integer.
def goal : Prop :=
{ d : ℤ | Squarefree d ∧ d > 1 ∧ IsClassNumberOne d }.InfiniteFrom Mathlib
import Conjectura.Problems.WP0008.Statement · maintainer — open · raw source
Adapted for Conjectura from formal-conjectures (Google DeepMind), `Wikipedia/ClassNumberProblem.lean`. The problem is catalogued at https://en.wikipedia.org/wiki/Class_number_problem. LOCKED: solvers cannot modify this file.
Copyright (c) 2025 The Formal Conjectures Authors. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: The Formal Conjectures Authors