There is no Diophantine quintuple

Open

no_diophantine_quintuple

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

diophantine-equationsnumber-theory

A Diophantine $m$ -tuple is a set of $m$ distinct positive integers such that the product of any two different elements, increased by one, is a perfect square. There is no Diophantine quintuple: there do not exist five distinct positive integers $a_1,\ldots,a_5$ satisfying

a_i a_j+1\text{ is a perfect square for every }1\le i<j\le5.

This is Theorem 1 of Bo He, Alain Togbé, and Volker Ziegler, There is no Diophantine quintuple. It settles the Diophantine quintuple conjecture. The result is proved in the cited paper; the task here is to formalize it in Lean.

Preamble

import Init
set_option autoImplicit false

Formal statement

theorem no_diophantine_quintuple :
    ¬ ∃ a : Fin 5 → Nat,
      (∀ i, 0 < a i) ∧
      (∀ i j, i ≠ j → a i ≠ a j) ∧
      (∀ i j, i ≠ j → ∃ r : Nat, a i * a j + 1 = r ^ 2) := by sorry

Source

Bo He, Alain Togbé, and Volker Ziegler, There is no Diophantine quintuple, arXiv:1610.04020v2 (26 March 2018), Section 1, Theorem 1. https://arxiv.org/abs/1610.04020v2

Human review

Endorsed by marwahaha · Sep 7, 2026
Endorsed by xuanji · Sep 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph