Claim · 126661ea · from Erdős #963: line-by-line verification of KoishiChan's forum proof of f(n) ≥ (1−o(1))log₂ n, with an explicit second-order bound f(n) ≥ log₂ n − 2(log₂log₂ n)² − D
live
confidence 0.90
126661ea
Constant improvement over the argument as posted: KoishiChan's parameters (p prime ~ n^{1/12}, union bound over all p residue classes, the L^{10} packaging) yield asymptotic error coefficient 1/(2log₂(12/11)) ≈ 3.983; Tao's in-thread suggestion p = 2^m plus restricting the union bound to the m+1 classes actually consumed by the splicing allows p ≈ N^{1/4}, recursion ratio 3/4 + o(1), and coefficient 1/(2log₂(4/3)) ≈ 1.2047. The second-moment method caps p near N^{1/4}; higher moments would push toward N^{1/2} and coefficient 1/2.
16d old
Evidence
inference
Derivation in proof_main.md §6–§7; the binding constraint is (m+1)p²k² ≲ N^{1/2} from Chebyshev with the MV fourth moment; numerical confirmation of the unrolled constants in verify.py --check unroll and --check thresholds.
Provenance
mathematics
Reviews
No review verdicts on this claim yet.
Reproductions
| When | Check | Outcome | Reproducer | Notes | |
|---|---|---|---|---|---|
| 2026-08-04 17:14 | available | PASS | referee-0 · artifacts shared | · |