---

Claim. The limit $\lim f(n)/n$ exists and is irrational, where $f(n)$ is the largest size of a subset of $\{1,\ldots,n\}$ in which no element divides two other distinct elements. The accepted formal statement is the formal-conjectures clause Erdos1062.erdos_1062.parts.ii with its open answer fixed to true: there is an $l$ with $f(n)/n\to l$ and $l$ irrational. The same file proves on the way an exact closed formula for $f(n)$ for every $n$, summing over the integers $q\le n$ coprime to $6$ the largest fork-free set of $\{2,3\}$-smooth numbers up to $n/q$ with a correction at finitely many scales per $q$, and identifies the limit as an explicit series, $0.6729656511994\ldots$, inside Lebensold's bracket $[0.6725,0.6736]$; the irrationality comes from a finiteness theorem for small integer combinations of numbers $2^a3^b$ (a parametric Subspace Theorem for the places $\infty$, $2$ and $3$) proved inside the file. The problem page states the formula, the series and the proof's four steps in full.

Submission note. Posted to erdosproblems.com as a proof claim by conjectures.io (account TFBloom) on 27 September 2026, giving "Unknown" as the AI used:

This formalisation claims a proof that the limit exists and is irrational. Notes: This was posted on conjectures.io. I have not verified the proof yet, and do not claim that the formalisation is correct, nor have I looked into the proof at all. I am posting this here so that others are aware that this claim has been made, and we can discuss it here. This should also not be read as any kind of endorsement of the conjectures.io program - in my view it is using these problems, which it does not care about, for its own ends, without making any attempts to explain these proofs or engage with the mathematical community. It is also not transparent (e.g. of who is running these through the AI, how long for, and which AI).

Claimant. The submission is filed on Conjectures.io under the username JenW1N, and the record's attribution field names conjectures.io; the proof file's header names no author and declares no AI system. A thread post of 23 September 2026 on erdosproblems.com reports the site's Lean-verified solution of the irrationality question under that username, and the site's proof-claim entry of 27 September 2026, registered by the curator, Thomas Bloom, attributes the claim to conjectures.io with the AI system given as unknown and points at the same Conjectures.io solution as a formalization claiming that the limit exists and is irrational; the entry's note says that the program does not disclose who runs the AI, for how long, or which system.

Acceptance. The accepting body is the bounty site Conjectures.io, whose record shows the proof verified by its Lean kernel, approved in review on 22 September 2026 under its policy v3, certified on 23 September 2026, and its bounty paid. The review's own note says it rested on the recorded production verification, integrity checks, selected proof interfaces and bounded prior-work searches, not on a fresh kernel replay or a complete line-by-line audit; that one Codex assessment was completed, without multiple independent assessments or an independent-consensus claim, and a human operator accepted the advisory recommendation; that the verdict rests on one kernel, a second kernel not being required for the task; and that Davis's April 2026 paper establishes the limit and leaves irrationality open, so the target was unresolved before this proof. The certifying body is the platform's review process, which examined a submission filed under the username JenW1N; the platform publishes the result under its own attribution, so the submitter and the reviewer are distinct while the reviewer and the published attribution coincide. This certification is a documented acceptance by an outside body and is listed as reviewed. There is no refereed version; the erdosproblems.com page showed OPEN on 2026-10-07, its curator's proof-claim entry says that the curator has not verified the proof and does not endorse the Conjectures.io program, so the curator's credit is not among the evidence, and the catalog's statement file, at the commit linked below, tags the clause research open. Nothing is independently reviewed by this project. Formalization. The 74,209-line proof file was not built here: its target, header and key declarations agree with the site's statement and the catalog's statement file (not itself a formalization), the file contains no sorry, axiom declaration, native_decide or unsafe option, the exact formula was confirmed by brute force for $n\le42$ and the series summed to the stated value; the deep components rest on the site's single kernel. Because no kernel check was reproduced here and the site's record itself notes the single kernel, formalized is not listed; the site's kernel acceptance is part of the review recorded above.

Scope. Full for the site's wording, which asks how large $f(n)$ can be and whether $\lim f(n)/n$ is irrational. The reviewed target asserts that $f(n)/n$ converges to an irrational limit, so the outside acceptance warrants both answers at the level of an irrational limiting density: $f(n)=(l+o(1))n$ for some irrational $l$. The claim value is answered, a yes to the irrationality question together with a determination of the size in asymptotic form; the site's curator read the asymptotic the same way when writing, on 4 May 2026, that Davis's result is not a full solution because the irrationality question remains. The exact formula for $f(n)$ and the explicit series value of $l$ are intermediate theorems of the same file, which the site's build compiled but its statement check and review did not examine; the problem page records them, with its recomputations, for information only, and the accepted standing does not rest on them.