What was already known
Choi, Erdős and Szemerédi proved only g₄(n)=O(1).
AI involvement
Van Doorn explicitly says GPT-5.3 Instant autonomously came up with the proof of Theorem 3 during brainstorming. Aristotle then formalized it in Lean. Van Doorn organized the paper and supplied human exposition; Aristotle's other formalizations and improved h₄ bound are separate contributions.
The author's first-person disclosure explicitly says GPT-5.3 Instant autonomously found the assessed Theorem 3 proof.
- Supporting source (github.com) — #866 partial-result row; wiki frozen June 30, 2026
Importance
Sharpens the four-integer case to an exact constant.
Limitations
The broader problem, including exact g₅, remains open. Van Doorn’s reported Lean formalization covers the four-integer theorem, not the harder five-integer case.
Technical verification
The author reports that each blue-checkmarked result, including Theorem 3, was formalized by Aristotle. The linked Lean file contains theorem g4 stating gFun 4 n = 3 for n≥2, with upper and lower lemmas and an axiom-print command. This review inspected the statement but did not build the file or audit all definitions.
Formal checking
Formal proof in ErdosProblem866.lean, with separate upper/lower lemmas and #print axioms g4
- Checker
- Lean 4 kernel through Aristotle, reported by Wouter van Doorn
- Scope
- ErdosProblem866.g4: gFun 4 n = 3 for all n≥2
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Van Doorn gives a short human-readable parity lower bound and pigeonhole upper bound, including explicit four-integer formulas, explaining the proof mechanism.
Correction and publication history
Sharpens the four-integer case to an exact constant.
Read this published revision