FormalConjectures.Wikipedia.DiophantineTuple

FormalConjectures
Wikipedia
DiophantineTuple

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module

public import FormalConjecturesUtil

Diophantine $m$-tuples

A Diophantine $m$-tuple is a set of $m$ distinct positive integers ${a_1, \dots, a_m}$ such that $a_i a_j + 1$ is a perfect square for every $i \neq j$.

References:

Wikipedia

[Du16] Dujella, Andrej, What is... a Diophantine m-tuple?, Notices Amer. Math. Soc. 63 (2016), 772--774.

[Du] Dujella, Andrej, Diophantine quintuple conjecture.

[HTZ19] He, Bo, Togbé, Alain and Ziegler, Volker, There is no Diophantine quintuple, Trans. Amer. Math. Soc. 371 (2019), 6665--6709.

[BD69] Baker, Alan and Davenport, Harold, The equations $3x^2-2=y^2$ and $8x^2-7=z^2$. Quart. J. Math. Oxford Ser. (2) 20 (1969), 129--137.

[Gi99] Gibbs, Philip, Some rational Diophantine sextuples, (1999).

@[expose] public sectionnamespace DiophantineTuplevariable {R : Type*} [Semiring R]

A finite set s is a Diophantine tuple if each element is nonzero and the product of any two distinct elements is one less than a perfect square.

We define this for all semirings and specialize to the integral and rational cases in this file; these are the most common in the literature. Note that the cases of ℕ and ℕ+ are mathematically equivalent.

def IsDiophantineTuple (s : Finset R) : Prop :=
  (∀ x ∈ s, x ≠ 0) ∧
  ∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsSquare (x * y + 1)

An integral Diophantine tuple is a Diophantine tuple of positive integers.

abbrev IsIntegralDiophantineTuple (s : Finset ℕ) : Prop := IsDiophantineTuple (R := ℕ) s

A rational Diophantine tuple is a Diophantine tuple of nonzero rationals.

abbrev IsRationalDiophantineTuple (s : Finset ℚ) : Prop := IsDiophantineTuple (R := ℚ) s

The property of being a Diophantine tuple is closed under subsets. [Du16]

@[category textbook, AMS 11]
theorem isDiophantineTuple_of_subset (s t : Finset R) (h1 : IsDiophantineTuple t)
    (h2 : s ⊆ t) : IsDiophantineTuple s :=
  ⟨fun x hx => h1.1 x (h2 hx), fun x hx y hy hxy => h1.2 x (h2 hx) y (h2 hy) hxy⟩

There exists a Diophantine 4-tuple; this example is due to Fermat.

@[category test, AMS 11]
theorem fermat_4_tuple : IsIntegralDiophantineTuple {1, 3, 8, 120} := by⊢ IsIntegralDiophantineTuple {1, 3, 8, 120}
  norm_num [IsDiophantineTuple]All goals completed! 🐙

The set of integral Diophantine 4-tuples.

def integralDiophantine4Tuple : Set (Finset ℕ) :=
  { s | IsIntegralDiophantineTuple s ∧ s.card = 4 }

/-- There exist infinitely many integral Diophantine 4-tuples. [Du16]

Proof: many parameterizations exist, e.g. ${k, k + 2, 4k + 4, 16k^3 + 48k^2 + 44k + 12}$.

@[category textbook, AMS 11]
example : integralDiophantine4Tuple.encard = ⊤ := byR:Type u_1inst✝:Semiring R⊢ integralDiophantine4Tuple.encard = ⊤ sorryAll goals completed! 🐙

The statement that there is no integral Diophantine 5-tuple.

abbrev NoIntegralDiophantineFiveTuple := ¬∃ t, IsIntegralDiophantineTuple t ∧ t.card = 5

The Diophantine 5-tuple theorem: there does not exist an integral Diophantine 5-tuple. [HTZ19]

@[category research solved, AMS 11]
theorem noIntegralDiophantineFiveTuple : NoIntegralDiophantineFiveTuple := by⊢ NoIntegralDiophantineFiveTuple sorryAll goals completed! 🐙

Given an integral Diophantine 3-tuple, there is a standard way to extend it to a 4-tuple by adjoining the value of this function. This is $d_+$ in [Du].

Note that when ${a, b, c}$ is a Diophantine tuple, each factor under the square root (e.g. $ab + 1$) is a perfect square.

def regularExtension (a b c : ℕ) : ℕ :=
  a + b + c + 2 * a * b * c + 2 * Nat.sqrt ((a * b + 1) * (a * c + 1) * (b * c + 1))

@[category test, AMS 11]
example : regularExtension 1 3 8 = 120 := byR:Type u_1inst✝:Semiring R⊢ regularExtension 1 3 8 = 120 norm_num [regularExtension]All goals completed! 🐙

The property that the Diophantine 3-tuple ${a, b, c}$ extends to a 4-tuple ${a, b, c, d}$ with $d > \max(a, b, c)$ only via regularExtension.

def HasUniqueExtension (a b c : ℕ) : Prop :=
  (IsIntegralDiophantineTuple { a, b, c }) ∧
  ∀ d : ℕ, (IsIntegralDiophantineTuple { a, b, c, d }) → max a (max b c) < d →
    d = regularExtension a b c

The statement that every integral Diophantine triple of three distinct elements has a unique extension by a larger element.

abbrev HasUniqueExtensionOfForall :=
  ∀ a b c : ℕ, ({a, b, c} : Finset ℕ).card = 3 → IsIntegralDiophantineTuple {a, b, c} →
    HasUniqueExtension a b c

The "strong Diophantine 5-tuple conjecture", so-called because it implies the Diophantine 5-tuple theorem (see noIntegralDiophantineFiveTuple_of_hasUniqueExtensionOfForall). [Du]

@[category research open, AMS 11]
theorem hasUniqueExtension_of_forall : HasUniqueExtensionOfForall := by⊢ HasUniqueExtensionOfForall sorryAll goals completed! 🐙

If every integral Diophantine triple has a unique extension by a larger element, then there is no integral Diophantine 5-tuple. [Du]

Proof: suppose a 5-tuple $a < b < c < d_1 < d_2$ exists; then $d_1 = d_2$ by unique extension.


@[category textbook, AMS 11]
theorem noIntegralDiophantineFiveTuple_of_hasUniqueExtensionOfForall :
    HasUniqueExtensionOfForall → NoIntegralDiophantineFiveTuple := by⊢ HasUniqueExtensionOfForall → NoIntegralDiophantineFiveTuple
  rintro h ⟨t, ht, hcard⟩h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5⊢ False
  set g := t.orderEmbOfFin hcard with hgh:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcard⊢ False
  have hm : StrictMono g := (t.orderEmbOfFin hcard).strictMonoh:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑g⊢ False
  have hmem : ∀ i, g i ∈ t := fun i => t.orderEmbOfFin_mem hcard ih:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ t⊢ False
  have h01 : g 0 < g 1 := hm (byh:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ t⊢ 0 < 1h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1⊢ False decideAll goals completed! 🐙h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1⊢ False)h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1⊢ False
  have h12 : g 1 < g 2 := hm (byh:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1⊢ 1 < 2h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2⊢ False decideAll goals completed! 🐙h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2⊢ False)h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2⊢ False
  have h23 : g 2 < g 3 := hm (byh:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2⊢ 2 < 3h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3⊢ False decideAll goals completed! 🐙h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3⊢ False)h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3⊢ False
  have h34 : g 3 < g 4 := hm (byh:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3⊢ 3 < 4h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4⊢ False decideAll goals completed! 🐙h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4⊢ False)h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4⊢ False
  have hs3 : ({g 0, g 1, g 2} : Finset ℕ) ⊆ t := by⊢ HasUniqueExtensionOfForall → NoIntegralDiophantineFiveTupleh:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ t⊢ False
    simp [Finset.insert_subset_iff, hmem]h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ t⊢ Falseh:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ t⊢ False
  have hs4 : ({g 0, g 1, g 2, g 3} : Finset ℕ) ⊆ t := by⊢ HasUniqueExtensionOfForall → NoIntegralDiophantineFiveTupleh:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ ths4:{g 0, g 1, g 2, g 3} ⊆ t⊢ False
    simp [Finset.insert_subset_iff, hmem]h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ ths4:{g 0, g 1, g 2, g 3} ⊆ t⊢ Falseh:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ ths4:{g 0, g 1, g 2, g 3} ⊆ t⊢ False
  have hs4' : ({g 0, g 1, g 2, g 4} : Finset ℕ) ⊆ t := by⊢ HasUniqueExtensionOfForall → NoIntegralDiophantineFiveTupleh:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ ths4:{g 0, g 1, g 2, g 3} ⊆ ths4':{g 0, g 1, g 2, g 4} ⊆ t⊢ False
    simp [Finset.insert_subset_iff, hmem]h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ ths4:{g 0, g 1, g 2, g 3} ⊆ ths4':{g 0, g 1, g 2, g 4} ⊆ t⊢ Falseh:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ ths4:{g 0, g 1, g 2, g 3} ⊆ ths4':{g 0, g 1, g 2, g 4} ⊆ t⊢ False
  have hc3 : ({g 0, g 1, g 2} : Finset ℕ).card = 3 :=
    Finset.card_eq_three.mpr ⟨_, _, _, h01.ne, (h01.trans h12).ne, h12.ne, rfl⟩h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ ths4:{g 0, g 1, g 2, g 3} ⊆ ths4':{g 0, g 1, g 2, g 4} ⊆ thc3:{g 0, g 1, g 2}.card = 3⊢ False
  obtain ⟨-, hu⟩ := h (g 0) (g 1) (g 2) hc3 (isDiophantineTuple_of_subset (R := ℕ) _ _ ht hs3)h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ ths4:{g 0, g 1, g 2, g 3} ⊆ ths4':{g 0, g 1, g 2, g 4} ⊆ thc3:{g 0, g 1, g 2}.card = 3hu:∀ (d : ℕ),
  IsIntegralDiophantineTuple {g 0, g 1, g 2, d} →
    max (g 0) (max (g 1) (g 2)) < d → d = regularExtension (g 0) (g 1) (g 2)⊢ False
  have e1 : g 3 = regularExtension (g 0) (g 1) (g 2) := by⊢ HasUniqueExtensionOfForall → NoIntegralDiophantineFiveTupleh:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ ths4:{g 0, g 1, g 2, g 3} ⊆ ths4':{g 0, g 1, g 2, g 4} ⊆ thc3:{g 0, g 1, g 2}.card = 3hu:∀ (d : ℕ),
  IsIntegralDiophantineTuple {g 0, g 1, g 2, d} →
    max (g 0) (max (g 1) (g 2)) < d → d = regularExtension (g 0) (g 1) (g 2)e1:g 3 = regularExtension (g 0) (g 1) (g 2)⊢ False
    refine hu _ (isDiophantineTuple_of_subset (R := ℕ) _ _ ht hs4) ?_h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ ths4:{g 0, g 1, g 2, g 3} ⊆ ths4':{g 0, g 1, g 2, g 4} ⊆ thc3:{g 0, g 1, g 2}.card = 3hu:∀ (d : ℕ),
  IsIntegralDiophantineTuple {g 0, g 1, g 2, d} →
    max (g 0) (max (g 1) (g 2)) < d → d = regularExtension (g 0) (g 1) (g 2)⊢ max (g 0) (max (g 1) (g 2)) < g 3h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ ths4:{g 0, g 1, g 2, g 3} ⊆ ths4':{g 0, g 1, g 2, g 4} ⊆ thc3:{g 0, g 1, g 2}.card = 3hu:∀ (d : ℕ),
  IsIntegralDiophantineTuple {g 0, g 1, g 2, d} →
    max (g 0) (max (g 1) (g 2)) < d → d = regularExtension (g 0) (g 1) (g 2)e1:g 3 = regularExtension (g 0) (g 1) (g 2)⊢ False
    simp only [max_eq_right h12.le]h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ ths4:{g 0, g 1, g 2, g 3} ⊆ ths4':{g 0, g 1, g 2, g 4} ⊆ thc3:{g 0, g 1, g 2}.card = 3hu:∀ (d : ℕ),
  IsIntegralDiophantineTuple {g 0, g 1, g 2, d} →
    max (g 0) (max (g 1) (g 2)) < d → d = regularExtension (g 0) (g 1) (g 2)⊢ max (g 0) (g 2) < g 3h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ ths4:{g 0, g 1, g 2, g 3} ⊆ ths4':{g 0, g 1, g 2, g 4} ⊆ thc3:{g 0, g 1, g 2}.card = 3hu:∀ (d : ℕ),
  IsIntegralDiophantineTuple {g 0, g 1, g 2, d} →
    max (g 0) (max (g 1) (g 2)) < d → d = regularExtension (g 0) (g 1) (g 2)e1:g 3 = regularExtension (g 0) (g 1) (g 2)⊢ False
    omegah:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ ths4:{g 0, g 1, g 2, g 3} ⊆ ths4':{g 0, g 1, g 2, g 4} ⊆ thc3:{g 0, g 1, g 2}.card = 3hu:∀ (d : ℕ),
  IsIntegralDiophantineTuple {g 0, g 1, g 2, d} →
    max (g 0) (max (g 1) (g 2)) < d → d = regularExtension (g 0) (g 1) (g 2)e1:g 3 = regularExtension (g 0) (g 1) (g 2)⊢ Falseh:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ ths4:{g 0, g 1, g 2, g 3} ⊆ ths4':{g 0, g 1, g 2, g 4} ⊆ thc3:{g 0, g 1, g 2}.card = 3hu:∀ (d : ℕ),
  IsIntegralDiophantineTuple {g 0, g 1, g 2, d} →
    max (g 0) (max (g 1) (g 2)) < d → d = regularExtension (g 0) (g 1) (g 2)e1:g 3 = regularExtension (g 0) (g 1) (g 2)⊢ False
  have e2 : g 4 = regularExtension (g 0) (g 1) (g 2) := by⊢ HasUniqueExtensionOfForall → NoIntegralDiophantineFiveTupleh:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ ths4:{g 0, g 1, g 2, g 3} ⊆ ths4':{g 0, g 1, g 2, g 4} ⊆ thc3:{g 0, g 1, g 2}.card = 3hu:∀ (d : ℕ),
  IsIntegralDiophantineTuple {g 0, g 1, g 2, d} →
    max (g 0) (max (g 1) (g 2)) < d → d = regularExtension (g 0) (g 1) (g 2)e1:g 3 = regularExtension (g 0) (g 1) (g 2)e2:g 4 = regularExtension (g 0) (g 1) (g 2)⊢ False
    refine hu _ (isDiophantineTuple_of_subset (R := ℕ) _ _ ht hs4') ?_h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ ths4:{g 0, g 1, g 2, g 3} ⊆ ths4':{g 0, g 1, g 2, g 4} ⊆ thc3:{g 0, g 1, g 2}.card = 3hu:∀ (d : ℕ),
  IsIntegralDiophantineTuple {g 0, g 1, g 2, d} →
    max (g 0) (max (g 1) (g 2)) < d → d = regularExtension (g 0) (g 1) (g 2)e1:g 3 = regularExtension (g 0) (g 1) (g 2)⊢ max (g 0) (max (g 1) (g 2)) < g 4h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ ths4:{g 0, g 1, g 2, g 3} ⊆ ths4':{g 0, g 1, g 2, g 4} ⊆ thc3:{g 0, g 1, g 2}.card = 3hu:∀ (d : ℕ),
  IsIntegralDiophantineTuple {g 0, g 1, g 2, d} →
    max (g 0) (max (g 1) (g 2)) < d → d = regularExtension (g 0) (g 1) (g 2)e1:g 3 = regularExtension (g 0) (g 1) (g 2)e2:g 4 = regularExtension (g 0) (g 1) (g 2)⊢ False
    simp only [max_eq_right h12.le]h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ ths4:{g 0, g 1, g 2, g 3} ⊆ ths4':{g 0, g 1, g 2, g 4} ⊆ thc3:{g 0, g 1, g 2}.card = 3hu:∀ (d : ℕ),
  IsIntegralDiophantineTuple {g 0, g 1, g 2, d} →
    max (g 0) (max (g 1) (g 2)) < d → d = regularExtension (g 0) (g 1) (g 2)e1:g 3 = regularExtension (g 0) (g 1) (g 2)⊢ max (g 0) (g 2) < g 4h:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ ths4:{g 0, g 1, g 2, g 3} ⊆ ths4':{g 0, g 1, g 2, g 4} ⊆ thc3:{g 0, g 1, g 2}.card = 3hu:∀ (d : ℕ),
  IsIntegralDiophantineTuple {g 0, g 1, g 2, d} →
    max (g 0) (max (g 1) (g 2)) < d → d = regularExtension (g 0) (g 1) (g 2)e1:g 3 = regularExtension (g 0) (g 1) (g 2)e2:g 4 = regularExtension (g 0) (g 1) (g 2)⊢ False
    omegah:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ ths4:{g 0, g 1, g 2, g 3} ⊆ ths4':{g 0, g 1, g 2, g 4} ⊆ thc3:{g 0, g 1, g 2}.card = 3hu:∀ (d : ℕ),
  IsIntegralDiophantineTuple {g 0, g 1, g 2, d} →
    max (g 0) (max (g 1) (g 2)) < d → d = regularExtension (g 0) (g 1) (g 2)e1:g 3 = regularExtension (g 0) (g 1) (g 2)e2:g 4 = regularExtension (g 0) (g 1) (g 2)⊢ Falseh:HasUniqueExtensionOfForallt:Finset ℕht:IsIntegralDiophantineTuple thcard:t.card = 5g:Fin 5 ↪o ℕ := t.orderEmbOfFin hcardhg:g = t.orderEmbOfFin hcardhm:StrictMono ⇑ghmem:∀ (i : Fin 5), g i ∈ th01:g 0 < g 1h12:g 1 < g 2h23:g 2 < g 3h34:g 3 < g 4hs3:{g 0, g 1, g 2} ⊆ ths4:{g 0, g 1, g 2, g 3} ⊆ ths4':{g 0, g 1, g 2, g 4} ⊆ thc3:{g 0, g 1, g 2}.card = 3hu:∀ (d : ℕ),
  IsIntegralDiophantineTuple {g 0, g 1, g 2, d} →
    max (g 0) (max (g 1) (g 2)) < d → d = regularExtension (g 0) (g 1) (g 2)e1:g 3 = regularExtension (g 0) (g 1) (g 2)e2:g 4 = regularExtension (g 0) (g 1) (g 2)⊢ False
  omegaAll goals completed! 🐙

HasUniqueExtension is known to hold for certain triples, including ${1, 3, 8}$: this is essentially the Baker–Davenport theorem [BD69], which states that $120$ is the only integer $d$ such that ${1, 3, 8, d}$ is a Diophantine tuple. Together with a finite check ruling out $d < 8$, this shows that no integral Diophantine tuple properly extends ${1, 3, 8, 120}$.

@[category research solved, AMS 11]
theorem hasUniqueExtension_of_1_3_8 : HasUniqueExtension 1 3 8 := by⊢ HasUniqueExtension 1 3 8 sorryAll goals completed! 🐙

/-
Theorems and conjectures about the rational case
-/

/-- An example due to Euler which extends fermat_4_tuple, showing that hasUniqueExtension_of_1_3_8 requires integrality.

@[category test, AMS 11]
example : IsRationalDiophantineTuple {1, 3, 8, 120, 777480/8288641} := byR:Type u_1inst✝:Semiring R⊢ IsRationalDiophantineTuple {1, 3, 8, 120, 777480 / 8288641}
  norm_num [IsDiophantineTuple]All goals completed! 🐙

A known rational Diophantine 6-tuple. [Gi99]

@[category test, AMS 11]
theorem gibbs_6_tuple :
    IsRationalDiophantineTuple {11/192, 35/192, 155/27, 512/27, 1235/48, 180873/16} := by⊢ IsRationalDiophantineTuple {11 / 192, 35 / 192, 155 / 27, 512 / 27, 1235 / 48, 180873 / 16}
  norm_num [IsDiophantineTuple]All goals completed! 🐙

Does there exist a rational Diophantine 7-tuple? [Du16]

@[category research open, AMS 11]
theorem rational_7_tuple :
    answer(sorry) ↔ ∃ t, IsRationalDiophantineTuple t ∧ t.card = 7 := by⊢ True ↔ ∃ t, IsRationalDiophantineTuple t ∧ t.card = 7
  sorryAll goals completed! 🐙

end DiophantineTuple