Claims

../

2026_05_11_kovac: Kovač's note bounds the proportion of N up to X with f(N) at most delta N by exp(-e^((1/delta)^c)) uniformly in X, so f(N) = o(N) fails, even along every set of density one.

2026_06_22_principia_math: Principia Math's write-up proves that for every A at least 1 the represented N with f(N) > AN have positive lower density, so the limsup of f(N)/N is infinite; with a Lean formalization.

2026_10_03_chae_fraiture_hou_kovac_kudeba_shakov_vidal: A seven-author manuscript proves f defined for every N other than 2 and 5, that f(N) = o(N) fails in a strong sense, even for almost all N, and that the limsup of f(N)/N is infinite; with Lean of 33 of its 37 results.

2026_10_05_xu: Xu's Lean development proves that f(n) is not o(n), not o(n) on any set of density one, and that the limsup of f(n)/n is infinite on every density-one set; registered in the Palomar registry.

---