Erdős problem 1148 · problems.science

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$ ?

Sources

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1148.lean

Retained formal statement1 of 3

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).

FormalConjectures/ErdosProblems/1148.leanErdos1148.erdos_11481 lineExact file

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

SolvedStatement only, no proof

Sources

Search problems.science