What was already known
The prior upper control was O(R), while Sárközy had a lower construction of order R^(1/2−o(1)).
AI involvement
Chojecki's first-person problem post says he obtained the upper-bound proof with GPT-5.5 Pro and credits the model's weighting in the positive-definiteness argument. The record does not resolve exactly which prompts or derivations came from Chojecki, so AI-led is supported by their joint proof account, without an autonomy claim.
Chojecki's original first-person post attributes the central new upper-bound proof to work with GPT-5.5 Pro; the division of steps is not detailed enough for AI-autonomous.
- Supporting source (github.com) — Lean erdos953_upper and conditional intermediate theorems
Importance
Matches the known lower exponent for the measurable planar problem.
Limitations
The new contribution is the Poisson–Bessel/Delsarte upper bound; Sárközy’s lower construction is independent earlier work. Kovač reports checking the proof, and Hart formalized the upper bound in Lean.
Technical verification
Kovač explicitly says the original proof is correct after examining it, and Hart's Lean Main.lean states the exact upper bound with the Poisson formula discharged in the repository. The machine artifact was inspected for axioms/sorries in its project files but not rebuilt; the prior lower bound is separate.
Formal checking
Human examination, explanation and correctness judgment of the argument
- Checker
- Vjeko Kovač
- Scope
- Chojecki–GPT proof of the O(sqrt(R)) upper bound
- Basis
- Reported by the linked checker
Formal checking
Lean proof erdos953_upper in Erdos953Formalization/Main.lean, including a discharged Poisson circle-average formula
- Checker
- Lean 4 formalization by Allen Hart
- Scope
- There exists C>0 such that M(R)<=C sqrt(R) for R>=1
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Kovač identifies the positive-definiteness/Delsarte mechanism, and the later streamlined exposition spells out the direct continuous argument.
Correction and publication history
Matches the known lower exponent for the measurable planar problem.
Read this published revision