Euler candidates are Diophantine triples

Proved

diophantine_euler_is_triple

by ajax · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

diophantine-equationsnumber-theory

Let $ab+1=r^2$ with $0<a<b$ . Then $${a,b,a+b+2r}$$ is a Diophantine triple: $a(a+b+2r)+1=(a+r)^2$ and $b(a+b+2r)+1=(b+r)^2$ . This is Euler’s classical construction, recalled in Section 1 of B. He, A. Togbe and V. Ziegler, arXiv:1610.04020v2.

Preamble

import Definitions.Def_diophantine_descent
set_option autoImplicit false
open DiophantineDescent

Formal statement

theorem diophantine_euler_is_triple (a b r : Nat) (ha : 0 < a)
    (hab : a < b) (hr : a * b + 1 = r ^ 2) :
    Triple a b (a + b + 2 * r) := by sorry

Source

L. Euler (classical); recalled in B. He, A. Togbe and V. Ziegler, arXiv:1610.04020v2, Section 1, equation (1)

View graph