The board / number theory / #1148
Erdős Problem #1148
PROVED LEANdatabase updated 2026-03-17
The statement as posed is true, and a proof exists. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
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\).
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](https://www.erdosproblems.com/forum/thread/1148#post-4849). The linked formal proof (plby/lean-proofs) removes the Duke hypothesis; it is stated over `ℤ`, as `∃ N, ∀ n ≥ N, ∃ x y z : ℤ, n = x ^ 2 + y ^ 2 - z ^ 2 ∧ max (x ^ 2) (max (y ^ 2) (z ^ 2)) ≤ n`, which gives the statement below by taking absolute values.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/1148.Prizenone
Topicsnumber theory
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/1148
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.