Wikipedia · textbook · AMS 11

mediumknown result, no worker yet

Congruent Number

Theorem · not_congruentNumber_1

1 is not a congruent number, as proved by Fermat via infinite descent.

Formal statement · Lean 4.lean
theorem not_congruentNumber_1 : ¬ congruentNumber 1 := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗