Claims

../

1975_01_01_bleicher_erdos: Bleicher and Erdős's Corollary 3: log S(N) is at least N log 2 / log N times the iterated-logarithm product up to depth k, when log_k N >= k; below the order of magnitude by an unbounded factor.

1976_12_01_bleicher_erdos: Bleicher and Erdős's Theorem 3: log S(N) is at most N log_r N / log N times the iterated-logarithm product up to depth r, when log_{2r} N >= 1; above the order of magnitude by an unbounded factor.

2025_09_12_bettin_grenie_molteni_sanna: Bettin, Grenié, Molteni and Sanna's Theorem 1: log S(N) is at least 2 log 2 times N / log N times the iterated-logarithm product, for every depth k >= 4 with log_k N >= 3/2; the lower half of the order of magnitude.

2026_07_15_young_zhu_luo: Young, Zhu and Luo's AI-assisted proof that log S(N) has the order of N / log N times the product of the iterated logarithms from the third to the last one exceeding 1, matching the refereed lower bound; site-accepted.

2026_07_22_kominers_neu: Kominers and Neu's AI-assisted claim of an asymptotic formula for log S(N) with a non-constant periodic phase factor and a second-order term, with a Lean 4 development resting on isolated assumptions; not accepted.

---