Claims

../

1982_01_01_erdos_guy_selfridge: Erdős, Guy and Selfridge prove constants 0 < c1 < c2 with 2n + c1 n/log n < f(n) < 2n + c2 n/log n for all large n, so f(n) - 2n has exact order n/log n; a proceedings paper, pending acceptance.

2026_05_02_mausberg: A note by Samuel Mausberg, written with GPT-5.5 Pro, proves that the liminf of (f(n) - 2n) log n / n is at least C0 = 4029639598/25970038185, a lower bound only; it neither proves an upper bound nor that the constant exists.

2026_07_18_wang: A manuscript found by GPT-5.6 Sol and submitted by Shouqiao Wang claims that f(n) - 2n is asymptotic to C0 n/log n with C0 = 4029639598/25970038185, with a Lean development this corpus has not built; no outside reviewer accepts it.

---