Overview

This project gives a completed Lean 4/mathlib formalization of the main theorem of A uniform bound of five for Diophantine tuples in imaginary quadratic integer rings by Zrinka Franušić and Tomislav Pejković.

A Diophantine tuple, or $D(1)$-tuple, in a commutative ring with identity is a finite set of nonzero elements such that $ab+1$ is a square in the ring whenever $a$ and $b$ are distinct elements of the set. The theorem gives a uniform upper bound of five for such tuples in the full rings of integers of all imaginary quadratic number fields.

Mathematical setting

Let $K$ be an imaginary quadratic number field, that is, an extension of $\mathbb Q$ of degree two that admits no embedding into $\mathbb R$. Let $\mathcal O_K$ denote its full ring of integers, consisting of the elements of $K$ that are integral over $\mathbb Z$.

A finite set $S\subseteq\mathcal O_K\setminus\{0\}$ is a $D(1)$-tuple if

$$\forall a,b\in S,\quad a\ne b\ \Longrightarrow\ \exists r\in\mathcal O_K,\quad r^2=ab+1.$$

The value $ab+1=0$ is allowed, with $r=0$. Requiring the square roots to lie in $K$ instead of $\mathcal O_K$ gives the same notion, since $\mathcal O_K$ is integrally closed in $K$.

Main theorem

For every imaginary quadratic number field $K$ and every $D(1)$-tuple $S$ in $\mathcal O_K$,

$$|S|\le 5.$$

Equivalently, $\mathcal O_K$ contains no $D(1)$-tuple with six elements.

Adžaga established a uniform bound of $42$. Cipu and Fujita established bounds of $24$ in 2024 and $22$ in 2026. Whether a $D(1)$-tuple with five elements exists in the ring of integers of any imaginary quadratic field remains an open question (Dujella, Problem 1.11).

Scope

The theorem concerns the full ring of integers in every case. In particular, for a positive squarefree integer $d\equiv3\pmod4$, it applies to $K=\mathbb Q(\sqrt{-d})$, whose ring of integers strictly contains $\mathbb Z[\sqrt{-d}]$. No further hypotheses are imposed on the entries.

Lean formalization

The formalization is complete. The main theorem has status Proved on Prove2Me. The formalization was completed on 24 October 2026. The Lean source repository contains the full source code and instructions for reproducing the verification.

The theorem card displays the formal statement with a by sorry placeholder; the accepted proof is stored separately and can be followed through its dependency graph.

The Lean 4 development D1Bound5 uses mathlib's full ring of integers 𝓞 K. Its main declaration is D1Bound5.main_statement, whose type is D1Bound5.MainStatement.

The proposition D1Bound5.MainStatement quantifies over types K with instances Field K, NumberField K and NumberField.IsTotallyComplex K, subject to Module.finrank ℚ K = 2, and over finite sets A : Finset (𝓞 K). It asserts A.card ≤ 5 whenever D1Bound5.IsD1 A holds. The definition D1Bound5.IsD1 requires every member to be nonzero and, for distinct members x and y, a witness r in the same ring satisfying r * r = x * y + 1.

Reference and source code

Zrinka Franušić and Tomislav Pejković, A uniform bound of five for Diophantine tuples in imaginary quadratic integer rings, preprint, 15 October 2026.

Lean formalization