Claims

../

2026_07_24_price: A proof claim posted by Liam Price, produced with GPT-5.6 Sol Pro, that infinitely many practical n have h(n) at most a constant times (log log n)^2, answering the first question; an unaccepted Overleaf draft.

2026_09_16_jenw1n: A kernel-checked Lean proof, certified by the bounty site Conjectures.io, that for every positive epsilon h(n!) < n^epsilon for all large n, which answers the second of the problem's three questions.

2026_09_16_van_doorn: Infinitely many practical n have h(n) at most c0 (log log n)^2 with c0 = 14/log 2, by an elementary extension construction with an author-side Lean formalization; a claimed answer to the first question, not accepted.

---