Theorem 7 — exclusion of the Euler case

Open

diophantine_quintuple_degree_zero

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

diophantine-equationsnumber-theory

Let $a<b<c<d<e$ be positive integers whose pairwise products plus one are perfect squares. Such a quintuple cannot exist when its smallest triple satisfies

\deg(a,b,c)=0.

Degree zero is precisely the Euler case. This is one of the three exclusions in the final degree classification.

Formalization Note The statement concerns extensions by two larger integers, the specialization needed for the headline theorem. Degree is represented by the finite descent relation.

Preamble

import Definitions.Def_diophantine_descent
set_option autoImplicit false
open DiophantineDescent

Formal statement

theorem diophantine_quintuple_degree_zero (f : Fin 5 → Nat) (hq : Quintuple f) (ho : Ordered f) (hd : HasDegree (f 0) (f 1) (f 2) 0) : False := by sorry

Source

Bo He, Alain Togbé, Volker Ziegler, There is no Diophantine quintuple, arXiv:1610.04020v2, https://arxiv.org/abs/1610.04020v2; Section 8, Theorem 7, specialized to the smallest three entries of an ordered quintuple; Section 4, degree definition.

View graph