Claims

../

1977_06_01_lebensold: Lebensold's 1977 bound 0.6725 n <= f(n) <= 0.6736 n for all large n, from a decomposition of {1, ..., n} into divisibility chains; refereed in Studies in Applied Mathematics.

2026_04_19_davis: Davis's arXiv paper of 19 April 2026 proves f(n) = c n + o(n) for an effectively computable constant c, answering how large f(n) can be in asymptotic form and leaving irrationality open; an unrefereed preprint.

2026_04_20_chojecki: A note dated 15 April 2026, generated with GPT-5.4 Pro and posted by Przemek Chojecki on 20 April 2026, proving f(n) = lambda n + o(n) with lambda effectively computable; unreviewed.

2026_09_21_jenw1n: A Lean proof submitted to the bounty site Conjectures.io under the username JenW1N, kernel-verified there on 21 September 2026 and certified on 23 September 2026, proves that f(n)/n converges to an irrational limit.

2026_09_23_turturean: A thread post of 23 September 2026 announces an independent manuscript giving an extremal formula for f(n) and the transcendence, hence irrationality, of the limit of f(n)/n, with the argument credited to GPT-6-Astra Pro; unreviewed.

---