Global bounds for a quintuple (Proposition 5)

Open

diophantine_quintuple_global_bound

by xuanji · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

diophantine-equationsnumber-theory

Let $a<b<c<d<e$ be a Diophantine quintuple. Then

ac<6.77\cdot 10^{{25}}\quad\text{and}\quad d<1.83\cdot 10^{{52}}.

This is the numerical part of Proposition 5 (Section 7), proved via linear forms in logarithms (Theorems 5–6). It is the shared global estimate used by the proofs of Theorems 8 and 9 to cap the subsequent finite searches; the companion Pell-exponent bound is stated separately.

Preamble

import Definitions.Def_diophantine_descent
set_option autoImplicit false
open DiophantineDescent

Formal statement

theorem diophantine_quintuple_global_bound (f : Fin 5 → Nat)
    (hq : Quintuple f) (ho : Ordered f) :
    f 0 * f 2 < 67700000000000000000000000 ∧ f 3 < 18300000000000000000000000000000000000000000000000000 := by sorry

Source

Bo He, Alain Togbé, Volker Ziegler, There is no Diophantine quintuple, arXiv:1610.04020v2, https://arxiv.org/abs/1610.04020v2; Section 7, Proposition 5 (bounds

ac<6.77\cdot 10^{25}

d<1.83\cdot 10^{52}

View graph