Motivation: when pairwise square conditions limit a set

Diophantine equations ask for integer solutions to arithmetic equations. One family of questions starts with a set of positive integers and imposes the same condition on every pair: their product, increased by one, must be a square. The question is how many distinct integers can satisfy all those conditions together. It connects a simple definition with a global restriction on simultaneous integer solutions.

The paper There is no Diophantine quintuple, by Bo He, Alain Togbé, and Volker Ziegler, resolves the nonexistence question for sets of five elements. This mission targets its headline result, Theorem 1 in Section 1. The mathematical theorem is proved in the paper; the remaining goal is a complete Lean proof of that result.

Setting: positive integers and pairwise perfect squares

A perfect square is an integer of the form $r^2$ for a natural number $r$. A Diophantine $m$-tuple is a set of $m$ distinct positive integers such that the product of any two different members, plus one, is a perfect square. Here $m$ records the number of elements, not a bound on their sizes. A Diophantine quintuple would have exactly five members (definition in Section 1).

Write those five integers as $a_1,\ldots,a_5$. Positivity means $a_i>0$ for every index. Distinctness means $a_i\ne a_j$ whenever $i\ne j$. The square condition requires a possibly different square root for each pair. There is no requirement that the ten square roots coincide, be distinct, or satisfy an additional ordering condition.

The theorem concerns positive integers. Replacing them by rational numbers changes the question. Likewise, allowing zero changes the admissible objects, and allowing repeated entries ceases to represent a five-element set. These domain choices are explicit in the formal target.

Formalization target: no Diophantine quintuple

The single goal is the following nonexistence statement:

$$\nexists\,a_1,\ldots,a_5\in\mathbb Z_{>0}\quad \left[ (\forall i\ne j,\ a_i\ne a_j) \ \land\ (\forall\,1\le i<j\le5,\ \exists r_{ij}\in\mathbb N,\ a_i a_j+1=r_{ij}^{,2}) \right].$$

This is Theorem 1 of the paper. The mission's goal is the existing declaration no_diophantine_quintuple.

The integers are unrestricted in size. The target does not fix the smallest entry, require a particular triple among the entries, or assume that an entry falls below a numerical search threshold. A proof must cover every quintuple satisfying the stated domain conditions.

Significance: an exact obstruction to larger sets

The result rules out an entire class of simultaneous square equations. As an immediate consequence, any set of distinct positive integers satisfying the same pairwise condition has at most four elements: a larger set would contain five distinct members that inherit the condition. This consequence explains why the five-element statement also constrains larger configurations.

A completed formalization would supply a reusable theorem that can be invoked whenever five distinct positive integers and their pairwise square witnesses arise. It would turn the informal nonexistence claim into a checked contradiction from precisely those hypotheses. The published statement is currently open for a Lean proof; its successful compilation verifies that the statement is well formed, not that the theorem has been proved.

Difficulty: the quantifier over all positive integers

Testing examples cannot establish this target by itself. Any computation with a fixed search limit addresses only a bounded collection, while the statement quantifies over all positive integers. A formal proof that uses a finite computation must also establish why the computation covers every possible case.

The conditions are simultaneous: each entry participates in four pairwise equations. Solving or excluding one isolated pair does not by itself settle whether all ten equations can hold together. The paper's proof overview in Section 2 describes the arithmetic estimates and computational components behind its result. Formalizing those components entails checking their hypotheses and connecting their conclusions to the unrestricted goal.

Formalization scope: five indexed natural numbers

The Lean declaration represents the entries by a function a : Fin 5 → Nat. It places the existence of that function under a negation and includes three conditions: every value is positive, different indices have different values, and every pair of different indices has a natural-number square witness.

The square condition is written for all unequal indices. This is equivalent to the usual condition for increasing pairs because multiplication is commutative. No increasing ordering of the five values is imposed. A development using sorted entries must justify its connection to this unrestricted indexed representation.

The root statement needs only Lean's core natural numbers, finite index type, arithmetic, and logic. It introduces no custom predicate whose meaning could hide additional assumptions. A complete proof may use Mathlib and reusable supporting results about integer arithmetic, squares, and the arithmetic tools required by the chosen argument. Supporting declarations should state their hypotheses explicitly and ultimately connect to this exact root theorem. Contributions establishing the known result, including an alternative rigorous proof, are within scope.

Selected references

• Bo He, Alain Togbé, and Volker Ziegler, There is no Diophantine quintuple, arXiv preprint, 2016; revised 2018, arXiv:1610.04020v2. Paper. The target is Section 1, Theorem 1; the definition precedes it, and Section 2 gives the proof overview.