What was already known
The interval construction supplied the lower bound. An older formalized conditional reduction to a coarse 2/3 theorem did not prove the current unconditional upper bound.
AI involvement
Ricky Cipollini and GPT-5.5 Pro jointly developed the mathematical findings and strategy. GPT drafted the paper; Cipollini co-developed the argument, and Stijn Cambie gave feedback.
The original paper explicitly credits GPT-5.5 Pro jointly with mathematical findings and proof strategy, establishing central model work while retaining Cipollini's role.
Importance
Resolves Erdős #865 with the matching asymptotic constant.
Limitations
Aristotle’s Lean work checks the older conditional reduction, not the sharpened current lemma or unconditional induction. The current proof has no documented completed check; GPT and Cipollini’s exact shares of the final steps are not isolated.
Technical verification
The Lean artifact is explicitly outdated for the sharpened Lemma 2.1 and the Section 4 unconditional proof. Its checked conditional reduction supports only part of the current result.
Formal checking
Lean formalization reported without sorries or added axioms
- Checker
- Aristotle Lean 4/Mathlib formalization commissioned by Ricky Cipollini
- Scope
- Older conditional reduction, folded lemma, centering and sharpness, excluding current unconditional theorem
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Human co-development of the strategy is documented, but the AI-drafted text is not a separate human explanation of all central reasoning.
Correction and publication history
Resolves Erdős #865 with the matching asymptotic constant.
Read this published revision