Exercise 5.11 — Every four consecutive integers contain a two-square gap

Proved

SteinENT.four_consecutive_gap

by wamlart · Sep 6, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

number-theory

For every integer $n$ , at least one member of the block $n,n+1,n+2,n+3$ is not a sum of two integer squares:

\exists k\in\{0,1,2,3\}\quad\nexists x,y\in\mathbb Z:\ n+k=x^2+y^2.

This gives a uniform bound on the length of consecutive runs of represented integers.

Preamble

import Mathlib.NumberTheory.SumTwoSquares
import Mathlib.NumberTheory.DiophantineApproximation.Basic
import Mathlib.Tactic

Formal statement

namespace SteinENT
theorem four_consecutive_gap (n : ℤ) :
    ∃ k : ℤ, 0 ≤ k ∧ k < 4 ∧ ¬ ∃ x y : ℤ, n + k = x ^ 2 + y ^ 2 := by sorry
end SteinENT

Source

William Stein, Elementary Number Theory: Primes, Congruences, and Secrets, author-hosted 2017 PDF, Exercise 5.11, printed pp. 122. https://wstein.org/ent/ent.pdf ; pinned author TeX commit c4984c7ddb22258674816f8c000b0d8eb485d694, body.tex lines 7183–7184: https://github.com/williamstein/ent/blob/c4984c7ddb22258674816f8c000b0d8eb485d694/body.tex

Read-back

What the Lean code literally says, in plain math · Codex (exact model identifier unavailable in auditor runtime)

Read-back model: unavailable (the exact runtime model identifier is not exposed).

For every integer $n$ , there exists an integer $k$ such that $0\le k$ , $k<4$ , and there do not exist integers $x,y$ with $n+k=x^2+y^2$ . Thus the asserted witness $k$ is one of $0,1,2,3$ , and at least one of the four integers $n,n+1,n+2,n+3$ has no representation as a sum of the squares of two integers. The starting integer $n$ is unrestricted, including $0$ and negative integers; neither $n$ nor $n+k$ is required to be positive or nonnegative. The integers $x,y$ range over all integers, including zero and negative values, with no coprimality or distinctness condition. Existence of at least one such offset is asserted, without uniqueness and without requiring every offset to have the stated property; there are no hypotheses or further assumptions.

Human review

Endorsed by Community (Bot) · Sep 6, 2026
Endorsed by wamlart · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph