Open on the site: the problem is labeled OPEN, with the site's note that it cannot be settled by a finite computation, and its commentary (last edited 6 January 2026) records only the trivial bound and Lebensold's bracket. The site's one proof-claim entry, registered on 27 September 2026 by the curator, Thomas Bloom, attributes to conjectures.io a proof, by an AI system the entry gives as unknown, that the limit exists and is irrational; the entry says that he has not verified it and that the program does not disclose who runs the AI or which system, so it is not an acceptance. The derived standing rests on the claim pages. A Lean proof submitted to the bounty site Conjectures.io under the username JenW1N, verified by the site's Lean kernel, approved in review on 22 September 2026 and certified on 23 September 2026 with its bounty paid (claim page (JenW1N, 2026), accepted), proves that $\lim f(n)/n$ exists and is irrational, which answers the second question yes and the first in asymptotic form, $f(n)=(l+o(1))\,n$ with $l$ irrational. Davis's paper of April 2026 gives $f(n)=c_2n+o(n)$ with $c_2$ effectively computable and leaves irrationality open (claim page (Davis, 2026), partial); a note generated with GPT-5.4 Pro and posted by Przemek Chojecki on 20 April 2026 proves the same with an explicit error term (claim page (Chojecki, 2026), partial). Lebensold's refereed bracket $0.6725n\le f(n)\le0.6736n$ for large $n$ (1977) is an accepted partial claim (claim page (Lebensold, 1977)). A manuscript announced in the thread on 23 September 2026 asserts an extremal formula for $f(n)$ and that the limit is transcendental (claim page (Turturean, 2026), full, unreviewed).