What was already known
The known lower exponent was 1/5; the best cited upper exponent was 1/4+o(1).
AI involvement
GPT-5.6 Sol proposed the projective normalization that lowers the density-increment dimension. Theofil Xeff adapted earlier results, wrote the proof and formalized it.
The original paper identifies one model-origin idea essential to closing the exponent gap, while the project and the cited density-increment framework remain human-led.
Importance
The upper bound determines the growth exponent of Erdős Problem 131.
Limitations
The Lean proof imports eight published results as axioms. Their correspondence to the cited theorems has not been independently audited.
Technical verification
The source reports a complete Lean 4 proof of the exact logarithmic-limit statement, conditional on eight explicitly named published theorem interfaces. The project lists their citations and axiom boundary.
Independent checking
Kernel-checked Lean proof with no sorry, statement/axiom audit and eight explicit cited external theorem axioms
- Checker
- Lean 4 kernel, reported by Xeff's erdos_131 project
- Scope
- Nondividing.main_log_limit: log F(N)/log N tends to 1/5 for the stated non-dividing definition
- Basis
- Reported by the linked checker
Human understanding
Xeff's paper explains how homogeneous progression coordinates preserve shell divisibility and why projective normalization lowers the dimension driving the exponent.
Correction and publication history
The upper bound determines the growth exponent of Erdős Problem 131.
Read this published revision