congruent_numbers_exact
Provedalgebraic-geometrydiophantineelliptic-curvesmillennium-prizenumber-theoryready-to-formalize
Congruent number problem: n is congruent iff the elliptic curve y² = x³ - n²x has a rational point of infinite order. Tunnell (1983) gave a criterion under BSD. Whether every squarefree n ≡ 5,6,7 (mod 8) is congruent remains open.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem congruent_numbers_exact :
∀ n : ℕ, 1 ≤ n →
((∃ a b c : ℚ, 0 < a ∧ 0 < b ∧ a ^ 2 + b ^ 2 = c ^ 2 ∧
a * b / 2 = n) ↔
(∃ x y : ℚ, y ^ 2 = x ^ 3 - (n : ℚ) ^ 2 * x ∧ y ≠ 0)) := by
sorrySource