Diophantine tuples

DefinitionDiophantine tuples#✓fully proved

A finite set \(s\) of natural numbers is a Diophantine tuple when every element of \(s\) is positive and, for all \(a, b \in s\) with \(a < b\), the number \(ab + 1\) is a perfect square.

def IsDiophantineTuple (s : Finset ℕ) : Prop :=
  (∀ a ∈ s, 0 < a) ∧ ∀ a ∈ s, ∀ b ∈ s, a < b → IsSquare (a * b + 1)

Sources

• OPG-16555 (Diophantine quintuple conjecture) [OpenGarden].

Used by 1

Used byThe statement that no Diophantine quintuple exists

DefinitionThe statement that no Diophantine quintuple exists#✓fully proved

The proposition that no finite set of natural numbers with exactly five elements is a Diophantine tuple, that is, that there is no Diophantine quintuple.

def Statement : Prop :=
  ¬∃ s : Finset ℕ, s.card = 5 ∧ IsDiophantineTuple s

Sources

• OPG-16555 (Diophantine quintuple conjecture) [OpenGarden].

Uses 1 · Used by 1

Statement usesDiophantine tuples

Used byThere is no Diophantine quintuple

TheoremThere is no Diophantine quintuple#●ready to prove

The statement that no Diophantine quintuple exists holds: no finite set of natural numbers with exactly five elements is a Diophantine tuple.

This was an open conjecture, resolved by He, Togbé, and Ziegler.

theorem_wanted Statement_holds : Statement

Sources

• Bo He, Alain Togbé, and Volker Ziegler, There is no Diophantine quintuple, Transactions of the American Mathematical Society 371 (2019), 6665–6709, https://doi.org/10.1090/tran/7573.

Uses 1

Statement usesThe statement that no Diophantine quintuple exists

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.