Prove2Me

Square witnesses in an Euler triple

Proved
euler_triple_square_identities

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

diophantine-equationsnumber-theory

Let a,b,r∈Na,b,r\in\mathbb{N} with ab+1=r2ab+1=r^2 and put c=a+b+2rc=a+b+2r (the Euler extension). Then

ac+1=(a+r)2andbc+1=(b+r)2,ac+1=(a+r)^2\quad\text{and}\quad bc+1=(b+r)^2,

i.e. the Euler triple carries explicit square witnesses. Pure algebra; used in Section 8 (Theorem 7) with s=a+rs=a+r and t=b+rt=b+r.

Formal statement
theorem euler_triple_square_identities (a b r : Nat) (h : a * b + 1 = r ^ 2) :
    a * (a + b + 2 * r) + 1 = (a + r) ^ 2 ∧ b * (a + b + 2 * r) + 1 = (b + r) ^ 2 := by sorry
Source
Bo He, Alain Togbé, Volker Ziegler, There is no Diophantine quintuple, arXiv:1610.04020v2, https://arxiv.org/abs/1610.04020v2; Section 8, Theorem 7 (identities s=a+rs=a+r, t=b+rt=b+r).

View graph