What was already known
Erdős asked whether the ratio diverges. Shengrong Wu earlier posted an AI-generated proof of two-sided constant-factor iterated-logarithm bounds; the exact 1/2 and 1 constants are the claimed further advance.
AI involvement
The repository credits GPT-5.5 Pro with the result statement, sketch and successor lemma, and Claude with manuscript assembly and Lean work. Turturean directed, assembled and audited the project.
Multiple original sources explicitly assign the central proof sketch, successor lemma and formalization to models; human assembly and checking remain material.
Importance
The claimed constants sharpen the earlier bounds and give a finite limiting ratio for Erdős 696.
Limitations
The full argument also relies on prime-chain estimates and imported analytic number theory. Turturean reports auditing the imported inputs, but no completed end-to-end check of the final theorem is documented.
Technical verification
The repository reports a sorry-free Lean formalization, but its main theorem depends on three external analytic-number-theory axioms. The three inputs remain assumptions in the formal theorem, and the source comparison does not establish a complete unconditional check.
Formal checking
Approximately 19,200-line sorry-free Lean development with three separately listed external axioms
- Checker
- Lean 4 compiler/kernel in Turturean's reported build
- Scope
- Formal Erdos696 main result conditional on the stated Siegel–Walfisz, Brun–Titchmarsh and Mertens inputs
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Default for missing evidence of full human grasp: Turturean describes trying to understand and rederive the proof, but no completed human explanation of the full exact-constant mechanism is documented in the sources reviewed.
Correction and publication history
The claimed constants sharpen the earlier bounds and give a finite limiting ratio for Erdős 696.
Read this published revision