Infinitude of Wall–Sun–Sun primes

Theorem · discr_rat_of_modEq_one

The discriminant of ℚ[√d] for d ≥ 2 squarefree congruent to 1 mod 4 is d.

Formal statement · Lean 4.lean

lemma discr_rat_of_modEq_one (hd₄ : d ≡ 1 [ZMOD 4]) : discr (QuadraticAlgebra ℚ d 0) = d := by
  sorry

Proof. sorry

Nobody has tried yet.