Congruent Number — open problem in number theory

Congruent Number

Tunnell's theorem (sufficient condition assuming BSD) for odd squarefree congruent numbers.

From the catalogue. Imported from The Formal Conjectures Authors (Google DeepMind and contributors) (Apache-2.0) — original. Nobody has started on it here yet: tasks are created as soon as someone asks for one or submits a claim.

Start working on it Submit a claim Follow

Cite

@misc{cairn-congruent-number,
  title        = {Congruent Number},
  author       = {{Cairn Commons contributors}},
  howpublished = {\url{https://cairn-commons.com/problems/congruent-number}},
  year         = {2026},
  note         = {Open problem on Cairn Commons, CC BY 4.0. Accessed 2026-09-29}
}

Also: CITATION.cff · Atom feed of results

Claims

Verified

Disputed

Refuted

On the literature board

The problem

The question

Tunnell_odd_converse. Tunnell's theorem (sufficient condition assuming BSD) for odd squarefree congruent numbers.

Tunnell_even_converse. Tunnell's theorem (sufficient condition assuming BSD) for even squarefree congruent numbers.

A natural number $n$ is called a congruent number if there exists a right triangle with rational sides $a$ , $b$ , and hypotenuse $c$ such that the area of the triangle is $\frac{1}{2} ab = n$ .

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Wikipedia.CongruentNumber (2 statements).

theorem Tunnell_odd_converse (n : ℕ) (hsqf : Squarefree n) (hodd : Odd n) :
    2 * (A n).ncard = (B n).ncard → congruentNumber n

theorem Tunnell_even_converse (n : ℕ) (hsqf : Squarefree n) (heven : Even n) :
    2 * (C n).ncard = (D n).ncard → congruentNumber n

What counts as progress

A Lean proof of one of the statements above, pinned as the claim's formal statement.
Partial results: special cases, weaker bounds, reductions — as verified claims.
Computations and numerical evidence with published code (reproducible).
Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

Source and licence

Imported from Formal Conjectures (Wikipedia), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.