What was already known
Eliahou and Revuelta had 14≤L(4)≤16 and conjectured L(n)=S(n−1)+1, predicting L(4)=14 and L(5)=45. Their separate recursive conjectures about Schur numbers remain open.
AI involvement
Adam McKenna reports that Claude Opus 5.5 produced the explicit sequence, group-partition lift, proofs, programs and Lean formalization under his direction; independent Claude agents audited them. McKenna is credited with directing and publishing the project.
Adam McKenna credits Claude Opus 5.5 with producing the sequence W, group-partition lift, proofs, checking programs and Lean formalization under his direction. McKenna directed and published the work.
Importance
Determines the previously open L(4) exactly and gives a general lower-bound construction for L(n), disproving a published conjecture at two values.
Limitations
The paper derives 49≤L(5)≤61 using a published Ramsey bound, but the Lean formalization checks only 49≤L(5)≤65 because that Ramsey bound is not formalized. The curated claim is L(4)=16 and L(5)≥49. The repository reports Lean-kernel finite checks and comparator checks. Independent Claude agents audited the work, while no completed human mathematical check is documented.
Technical verification
The source reports Lean-kernel and comparator checks for L(4)=16, the group-partition lift, and 49≤L(5)≤65. This covers the assessed L(4)=16 and L(5)≥49 claims. The stronger paper-only upper bound L(5)≤61 was not formalized and is excluded from this assessment.
Formal checking
Project reports Lean and comparator checks of the six advertised statement files; selected claims L(4)=16 and L(5)≥49 match the formalized lower bounds.
- Checker
- Lean 4 kernel and comparator as run by Adam McKenna and repository CI
- Scope
- L(4)=16, L(5)≥49 and the group-partition lift; excludes the paper-only L(5)≤61 upper bound
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
The paper gives a short explainable construction, but the available source documents Claude agents auditing it rather than a human explaining the central sequence and lift. Few is an evidence default, not a positive finding that humans cannot understand it.
Correction and publication history
Primary paper, project provenance and formalization scope reviewed; selected only the two new results matched by Lean, not the paper-only Ramsey upper bound.
Read this published revision