Erdős Problem 1148

References:

• erdosproblems.com/1148
• [Ch26] P. Chojecki, Bounded Representations by $x^2 + y^2 - z^2$ (2026)
• [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999).

def Erdos1148.Erdos1148Prop (n : ℕ) : Prop

A natural number $n$ which can be written as $n$ if $n = x^2 + y^2 - z^2$ with $\max(x^2, y^2, z^2) \leq n$.

Equations

• Erdos1148.Erdos1148Prop n = ∃ (x : ℕ) (y : ℕ) (z : ℕ), n = x ^ 2 + y ^ 2 - z ^ 2 ∧ x ^ 2 ≤ n ∧ y ^ 2 ≤ n ∧ z ^ 2 ≤ n

theorem Erdos1148.erdos_1148 : True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, Erdos1148Prop n

Can every large integer $n$ be written as $n=x^2+y^2-z^2$ with $\max(x^2,y^2,z^2)\leq n$?

This was proved affirmatively by Chojecki [Ch26], using a Duke-type equidistribution theorem. A Lean formalisation of the reduction (conditional on a Duke-type equidistribution theorem) exists; see the forum discussion.

theorem Erdos1148.erdos_1148.variants.lower_bound : ¬Erdos1148Prop 6563

The integer $6563$ cannot be written as $x^2 + y^2 - z^2$ with $\max(x^2, y^2, z^2) \leq 6563$.

def Erdos1148.erdos_1148_weaker_prop (n : ℕ) : Prop

The weaker property: $n = x^2 + y^2 - z^2$ such that $\max(x^2, y^2, z^2) \leq n + 2\sqrt{n}$.

Equations

• Erdos1148.erdos_1148_weaker_prop n = ∃ (x : ℕ) (y : ℕ) (z : ℕ), n = x ^ 2 + y ^ 2 - z ^ 2 ∧ ↑x ^ 2 ≤ ↑n + 2 * √↑n ∧ ↑y ^ 2 ≤ ↑n + 2 * √↑n ∧ ↑z ^ 2 ≤ ↑n + 2 * √↑n

theorem Erdos1148.erdos_1148.variants.weaker (n : ℕ) : erdos_1148_weaker_prop n

[Va99] reports this is 'obvious' if we replace $\leq n$ with $\leq n+2\sqrt{n}$.