Theorem 8 — exclusion of degree one

Open

diophantine_quintuple_degree_one

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

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_one (f : Fin 5 → Nat) (hq : Quintuple f) (ho : Ordered f) (hd : HasDegree (f 0) (f 1) (f 2) 1) : 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 9, Theorem 8, specialized to the smallest three entries of an ordered quintuple.

View graph