No Diophantine pair of consecutive integers
Proveddiophantine_pair_gapdiophantine-equationsnumber-theory
Consecutive positive integers never form a Diophantine pair: for , lies strictly between and and so is not a perfect square. Hence a Diophantine quintuple (or triple) always has ; together with Fujita’s result ruling out b-a=2—Y. Fujita, The extensibility of Diophantine pairs \{k-1,k+1}$, J. Number Theory 128 (2008)—this gives $b-a\ge 3—cf. M. Cipu and Y. Fujita, Bounds for Diophantine quintuples, Glas. Mat. 50 (2015), proof of Theorem 1.1.
Preamble
import Mathlib.Tactic
Formal statement
theorem diophantine_pair_gap (a r : Nat) (ha : 0 < a)
(h : a * (a + 1) + 1 = r ^ 2) : False := by sorrySource
M. Cipu and Y. Fujita, Bounds for Diophantine quintuples, Glas. Mat. 50 (2015), 25-34, proof of Theorem 1.1 (the b-a >= 3 reduction via [14])