Class number problem for real quadratic fields

Conjectura.Problems.WP0008.Statement

/-
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
-/
import Mathlib.NumberTheory.NumberField.ClassNumber

/-! # Class number problem for real quadratic fields

## Source

Adapted for Conjectura from [formal-conjectures](https://github.com/google-deepmind/formal-conjectures) (Google DeepMind), `Wikipedia/ClassNumberProblem.lean`. The problem is catalogued at [https://en.wikipedia.org/wiki/Class_number_problem](https://en.wikipedia.org/wiki/Class_number_problem).

LOCKED: solvers cannot modify this file.
-/

open Polynomial

namespace Conjectura.WP0008

def IsClassNumberOne (d : ℤ) : Prop :=
  ∃ (h₂ : Irreducible (X ^ 2 - C (d : ℚ))),
  haveI := Fact.mk h₂
  NumberField.classNumber (AdjoinRoot (X ^ 2 - C (d : ℚ))) = 1

/--
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
  sorry

/--
**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
  sorry

/-- 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 }.Infinite

end Conjectura.WP0008