---

Claim. There is an $N$ such that every integer $n\ge N$ has integers $x,y,z$ with $n=x^2+y^2-z^2$ and $\max(x^2,y^2,z^2)\le n$ (Theorem 1.1 of the note). This answers Problem 1148 affirmatively. The threshold $N$ is not explicit (Remark 5.1).

Source. P. Chojecki, Bounded representations by $x^2+y^2-z^2$, note dated 2026-03-16, posted to the site's forum the same day. The note names Chojecki as its author; in the thread Chojecki wrote that the proof came out of an exchange with GPT-5.4 Pro and was checked with Gemini 3.1, and the site credits Chojecki and GPT-5.4 Pro. An earlier note by the same author, Sieve methods and a problem of Erdős (2026-01-26), proved the representation for a density-one set of $n$ with $O(N^{3/4})$ exceptions up to $N$; the full note supersedes it.

The argument. Squares are trivial ($n=m^2+0^2-0^2$). For non-square $n$, the substitution $a=x+z$, $b=2y$, $c=z-x$ turns a representation into a binary quadratic form $[a,b,c]$ of discriminant $b^2-4ac=4n$ with $b$ even and $a\equiv c\pmod 2$, and the bound $\max(x^2,y^2,z^2)\le n$ into the condition that the scaled point $(a,b,c)/(2\sqrt n)$ lies in a fixed relatively compact open patch of the hyperboloid $B^2-4AC=1$. Duke's theorem, in the point-counting form the note deduces from Theorem 2.3 of Einsiedler, Lindenstrauss, Michel and Venkatesh, supplies a primitive form of discriminant $4n$ in a smaller patch for every large $n$; two explicit matrices preserving the discriminant then fix the parity of the coefficients while keeping the point in the patch, and the substitution is reversed.

Lean. The claimant's Lean 4 file (the first formalization link, posted 2026-03-17 as produced with Gemini 3.1, Opus 4.6, GPT-5.4 and the UlamAI prover) proves the theorem from a hypothesis DukeTheoremStatement, which asserts that for every large $n$ there is a primitive triple $(a,b,c)$ of discriminant $4n$ whose scaled point lies in the patch and whose first and third coefficients have equal parity. The file therefore checks the dictionary between such triples and representations and the bound on the three squares, while both the Duke input and the note's parity step (the two matrices) are assumed in the hypothesis; the file declares no axiom and has no sorry, but the hypothesis is not proved in Lean, and a thread comment of 2026-03-18 noted that the homogeneous dynamics it would need was not well represented in Mathlib. The site's label PROVED (LEAN) refers to this conditional development. The second formalization link is the file src/latest/ErdosProblems/Erdos1148.lean of Boris Alexeev's repository lean-proofs (Lean and Mathlib v4.33.0; 248 lines at the pinned commit), which declares itself a formalization of a solution to Problem 1148, unconditional, with the Duke hypothesis removed; it names GPT-5.4 Pro and Chojecki as informal authors, lists the tools of the original conditional formalization, keeps the conditional proof as erdos_1148_of_duke, derives the theorem erdos_1148 from a separately imported local-existence module, and records Alexeev as the author of the completing commit. The formal-conjectures statement erdos_1148 is tagged research solved and carries a formal_proof link to that pinned file, noting that it removes the Duke hypothesis. The unconditional claim is the file's own: this corpus has not built or audited either file, so the page lists no formalized evidence.

Acceptance. Reviewed: the site's curator, Thomas Bloom, marks the problem proved and credits Chojecki and GPT-5.4 Pro with the deduction from Duke's theorem on the problem page (last edited 2026-05-28); the community database records the status proved (Lean) from 2026-03-17. A thread comment of 2026-03-17 found the approach plausible; that is commentary on the method, not a review of the proof, and the acceptance recorded here is the curator's alone. No refereed publication of the note is recorded on the site or in the thread, and this corpus has not independently verified the proof.

Depends on. No page of this wiki; the proof rests on the cited 2012 paper, whose card is linked above.