Skip to content

Erdős problem 1148

Start work

Can every large integer nn be written as n=x2+y2−z2n=x^2+y^2-z^2 with max⁡(x2,y2,z2)≤n\max(x^2,y^2,z^2)\leq n?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1148.lean

Retained formal statement1 of 3

Can every large integer nn be written as n=x2+y2−z2n=x^2+y^2-z^2 with max⁡(x2,y2,z2)≤n\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.

FormalConjectures/ErdosProblems/1148.leanErdos1148.erdos_11481 lineExact file
True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, Erdos1148.Erdos1148Prop n
SolvedStatement only, no proof