DiophantineTuple.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

19 declarations, 5 contain sorry, 0 declared as axioms

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).

Imports (1)

FormalConjecturesUtil

def DiophantineTuple.IsDiophantineTuple 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 line 57 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Semiring, Finset
Proof uses: And, Membership.mem, Ne, OfNat.ofNat, IsSquare, HAdd.hAdd, HMul.hMul
15 instances, coercions and auxiliary constants left out.
```
def IsDiophantineTuple (s : Finset R) : Prop :=
…
```
abbrev DiophantineTuple.IsIntegralDiophantineTuple An integral Diophantine tuple is a Diophantine tuple of positive integers line 62 source
Source documentation
An integral Diophantine tuple is a Diophantine tuple of positive integers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: DiophantineTuple.IsDiophantineTuple
1 instances, coercions and auxiliary constants left out.
```
abbrev IsIntegralDiophantineTuple (s : Finset ℕ) : Prop := IsDiophantineTuple (R := ℕ) s
```
Mentions: DiophantineTuple.IsDiophantineTuple
abbrev DiophantineTuple.IsRationalDiophantineTuple A rational Diophantine tuple is a Diophantine tuple of nonzero rationals line 65 source
Source documentation
A rational Diophantine tuple is a Diophantine tuple of nonzero rationals.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Rat
Proof uses: DiophantineTuple.IsDiophantineTuple
1 instances, coercions and auxiliary constants left out.
```
abbrev IsRationalDiophantineTuple (s : Finset ℚ) : Prop := IsDiophantineTuple (R := ℚ) s
…
```
Mentions: DiophantineTuple.IsDiophantineTuple
theorem DiophantineTuple.isDiophantineTuple_of_subset The property of being a Diophantine tuple is closed under subsets line 71 source
Source documentation
The property of being a Diophantine tuple is closed under subsets. [Du16]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Semiring, Finset, DiophantineTuple.IsDiophantineTuple, LE.le
Proof uses: And.intro, Membership.mem, Ne, OfNat.ofNat, IsSquare, HAdd.hAdd, HMul.hMul, And.left, And.right
21 instances, coercions and auxiliary constants left out.
```
theorem isDiophantineTuple_of_subset (s t : Finset R) (h1 : IsDiophantineTuple t)
    (h2 : s ⊆ t) : IsDiophantineTuple s :=
…
```
Mentions: DiophantineTuple.IsDiophantineTuple
theorem DiophantineTuple.fermat_4_tuple There exists a Diophantine 4-tuple; this example is due to Fermat line 83 source
Source documentation
There exists a Diophantine 4-tuple; this example is due to Fermat.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DiophantineTuple.IsIntegralDiophantineTuple, Insert.insert, Nat, Finset, OfNat.ofNat, Singleton.singleton
Proof uses: of_eq_true, DiophantineTuple.IsDiophantineTuple, Eq.trans, And, Membership.mem, Ne, IsSquare, HAdd.hAdd, HMul.hMul, True, DiophantineTuple.IsDiophantineTuple.eq_1, congr, congrArg, Not, Eq, Or, forall_congr, implies_congr, Eq.refl, eq_true and 18 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem fermat_4_tuple : IsIntegralDiophantineTuple {1, 3, 8, 120} := by
…
```
Mentions: DiophantineTuple.IsIntegralDiophantineTuple
def DiophantineTuple.integralDiophantine4Tuple The set of integral Diophantine 4-tuples line 89 source
Source documentation
The set of integral Diophantine 4-tuples.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Finset, Nat
Proof uses: Set.ofPred, And, DiophantineTuple.IsIntegralDiophantineTuple, Eq, Finset.card, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def integralDiophantine4Tuple : Set (Finset ℕ) :=
…
```
example DiophantineTuple.(example at line 98) sorry line 98 source
Source documentation
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\}$.
```
example : integralDiophantine4Tuple.encard = ⊤ := by sorry
```
abbrev DiophantineTuple.NoIntegralDiophantineFiveTuple The statement that there is no integral Diophantine 5-tuple line 103 source
Source documentation
The statement that there is no integral Diophantine 5-tuple.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: Not, Exists, Finset, Nat, And, DiophantineTuple.IsIntegralDiophantineTuple, Eq, Finset.card, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
```
abbrev NoIntegralDiophantineFiveTuple := ¬∃ t, IsIntegralDiophantineTuple t ∧ t.card = 5
…
```
Mentions: DiophantineTuple.IsIntegralDiophantineTuple
theorem DiophantineTuple.noIntegralDiophantineFiveTuple The Diophantine 5-tuple theorem: there does not exist an integral Diophantine 5-tuple sorry line 109 source
Source documentation
The Diophantine 5-tuple theorem: there does not exist an integral Diophantine 5-tuple. [HTZ19]

depends on sorry what this means
Statement uses: DiophantineTuple.NoIntegralDiophantineFiveTuple
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem noIntegralDiophantineFiveTuple : NoIntegralDiophantineFiveTuple := by sorry
```
Mentions: DiophantineTuple.NoIntegralDiophantineFiveTuple
def DiophantineTuple.regularExtension 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 line 122 source
Source documentation
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.

no axioms what this means
Statement uses: Nat
Proof uses: HAdd.hAdd, HMul.hMul, OfNat.ofNat, Nat.sqrt
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def regularExtension (a b c : ℕ) : ℕ :=
…
```
Mentions: c
example DiophantineTuple.(example at line 126) line 126 source
def DiophantineTuple.HasUniqueExtension 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 line 132 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: And, DiophantineTuple.IsIntegralDiophantineTuple, Insert.insert, Finset, Singleton.singleton, LT.lt, Max.max, Eq, DiophantineTuple.regularExtension
5 instances, coercions and auxiliary constants left out.
```
def HasUniqueExtension (a b c : ℕ) : Prop :=
…
```
Mentions: c
abbrev DiophantineTuple.HasUniqueExtensionOfForall The statement that every integral Diophantine triple of three distinct elements has a unique extension by a larger element line 141 source
Source documentation
The statement that every integral Diophantine triple of three distinct elements has a unique extension by a larger element.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: Nat, Eq, Finset.card, Insert.insert, Finset, Singleton.singleton, OfNat.ofNat, DiophantineTuple.IsIntegralDiophantineTuple, DiophantineTuple.HasUniqueExtension
4 instances, coercions and auxiliary constants left out.
```
abbrev HasUniqueExtensionOfForall :=
…
```
theorem DiophantineTuple.hasUniqueExtension_of_forall The "strong Diophantine 5-tuple conjecture", so-called because it implies the Diophantine 5-tuple theorem (see noIntegralDiophantineFiveTuple_of_hasUniqueExtensionOfForall) sorry line 150 source
Source documentation
The "strong Diophantine 5-tuple conjecture", so-called because it implies the Diophantine 5-tuple theorem (see noIntegralDiophantineFiveTuple_of_hasUniqueExtensionOfForall). [Du]

depends on sorry what this means
Statement uses: DiophantineTuple.HasUniqueExtensionOfForall
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem hasUniqueExtension_of_forall : HasUniqueExtensionOfForall := by sorry
…
```
Mentions: DiophantineTuple.HasUniqueExtensionOfForall
theorem DiophantineTuple.noIntegralDiophantineFiveTuple_of_hasUniqueExtensionOfForall If every integral Diophantine triple has a unique extension by a larger element, then there is no integral Diophantine 5-tuple line 159 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DiophantineTuple.HasUniqueExtensionOfForall, DiophantineTuple.NoIntegralDiophantineFiveTuple
Proof uses: Exists, Finset, Nat, And, DiophantineTuple.IsIntegralDiophantineTuple, Eq, Finset.card, OfNat.ofNat, False, OrderEmbedding, Fin, Finset.orderEmbOfFin, rfl, StrictMono, OrderEmbedding.strictMono, Membership.mem, Finset.orderEmbOfFin_mem, LT.lt, of_decide_eq_true, id and 31 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
theorem noIntegralDiophantineFiveTuple_of_hasUniqueExtensionOfForall :
    HasUniqueExtensionOfForall → NoIntegralDiophantineFiveTuple := by
…
```
Mentions: DiophantineTuple.HasUniqueExtensionOfForall, DiophantineTuple.NoIntegralDiophantineFiveTuple
theorem DiophantineTuple.hasUniqueExtension_of_1_3_8 HasUniqueExtension is known to hold for certain triples, including sorry line 195 source
Source documentation
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\}$.

depends on sorry what this means
Statement uses: DiophantineTuple.HasUniqueExtension, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem hasUniqueExtension_of_1_3_8 : HasUniqueExtension 1 3 8 := by sorry
…
```
Mentions: DiophantineTuple.HasUniqueExtension
example DiophantineTuple.(example at line 206) line 206 source
Source documentation
An example due to Euler which extends fermat_4_tuple, showing that hasUniqueExtension_of_1_3_8 requires integrality.
```
example : IsRationalDiophantineTuple {1, 3, 8, 120, 777480/8288641} := by
…
```
Mentions: DiophantineTuple.IsRationalDiophantineTuple
theorem DiophantineTuple.gibbs_6_tuple A known rational Diophantine 6-tuple line 213 source
Source documentation
A known rational Diophantine 6-tuple. [Gi99]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DiophantineTuple.IsRationalDiophantineTuple, Insert.insert, Rat, Finset, HDiv.hDiv, OfNat.ofNat, Singleton.singleton
Proof uses: of_eq_true, Eq.trans, And, Membership.mem, Ne, IsSquare, HAdd.hAdd, HMul.hMul, True, congrArg, congr, Mathlib.Meta.NormNum.IsNNRat.to_eq, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, Inv.inv, Eq.refl, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.isNNRat_inv_pos, Nat and 32 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem gibbs_6_tuple :
    IsRationalDiophantineTuple {11/192, 35/192, 155/27, 512/27, 1235/48, 180873/16} := by
…
```
Mentions: DiophantineTuple.IsRationalDiophantineTuple
theorem DiophantineTuple.rational_7_tuple Does there exist a rational Diophantine 7-tuple? sorry line 221 source
Source documentation
Does there exist a rational Diophantine 7-tuple? [Du16]

depends on sorry what this means
Statement uses: Iff, True, Exists, Finset, Rat, And, DiophantineTuple.IsRationalDiophantineTuple, Eq, Nat, Finset.card, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem rational_7_tuple :
    answer(sorry) ↔ ∃ t, IsRationalDiophantineTuple t ∧ t.card = 7 := by
…
```
Mentions: DiophantineTuple.IsRationalDiophantineTuple