What was already known
Erdős, Guy and Selfridge established order n/log n for f(n)−2n. Mausberg later found the same thirteen-layer constant as a lower bound, without an upper bound or limit.
AI involvement
Wang credits GPT-5.6 with finding the proposed solution and authored the manuscript and repository. Mausberg supplied the earlier lower-bound constant.
The manuscript expressly credits GPT-5.6 with the proposed solution; the exact human mathematical input to the new upper-bound argument is not documented well enough to call it autonomous.
Importance
A matching upper bound would determine the previously unknown second-order constant.
Limitations
The problem record still lists #390 as open. A public Lean build passed for the stated asymptotic, while its match to the original factorization question and the new upper-bound argument await independent human scrutiny.
Technical verification
The cited Lean source exposes the assumption-free main asymptotic and the upper-endpoint estimate, and the July 28 CI run reports a successful Lean build at that commit. This is source-reported machine checking of the formal statement, not an independently replayed check of the mathematical translation. The finite allocation verifier covers only its certificate and cannot by itself prove the full asymptotic.
Formal checking
Repository Lean build, with the public expanded endpoint and theorem statement audit
- Checker
- Lean 4 CI for ShouqiaoW/erdos at commit 61325b1
- Scope
- Assumption-free asymptotic f(n) = 2n + C0*n/log(n) + o(n/log(n)), including the eventual matching upper endpoint
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
The manuscript describes proof components, but the reviewed sources do not document a named person's explanation of the new upper-bound mechanism. Few is the evidence default.
Correction and publication history
A matching upper bound would determine the previously unknown second-order constant.
Read this published revision