---

Claim. Call $A\subseteq\{1,\ldots,N\}$ admissible when no $a,b\in A$ satisfy $b=at$ with the least prime factor of $t$ larger than $a$, and let $M(N)$ be the largest value of $\sum_{n\in A}1/n$ over admissible $A$. Przemek Chojecki proves that

$$M(N)=(c_2+o(1))\log N,$$

so the quantity the problem asks about, $M(N)/\log N$, tends to the explicit constant $c_2=0.6187712111\ldots$. The constant is defined through the function

$$\Phi(u)=\log\frac{1-u}{u}+\int_u^{(1-u)/2}\frac{1}{v}\log\frac{1-u-v}{v}\,dv \qquad(\tfrac14\le u\le\tfrac12),$$

with the integral read as $0$ for $u\ge1/3$: $\alpha_2=0.28043830989\ldots$ is the unique solution of $\Phi(\alpha_2)=1$ in $(1/4,1/3)$, and $c_2=\tfrac12+\int_{\alpha_2}^{1/2}(1-\Phi(u))\,du$. The full note of 15 April 2026 (first link) proves, as its Theorem 1.1, that for every $N\ge2$ the optimum is attained by a frontier antichain of the relation $a\preceq b$ ($b=a$ or $b=at$ with the least prime factor of $t$ above $a$). The proof is a sign theorem in three parts: an exact computation of the thresholds for $a\le19$, the one computer-assisted step, a prime-harmonic bound for $20\le a\le N^{1/4}$, and a monotonicity argument above the $N^{1/4}$ layer; an independent analytic proof by a Bellman recursion, valid for large $N$ only, is given as well. The note then evaluates the frontier sweep, whose children are prime and semiprime extensions. The third note (third link) rewrites the second note's streamlined proof as a discrete divergence theorem for a reciprocal flow on the rooted tree of the relation: the reciprocal weight of an admissible antichain equals the total divergence of the upset it generates, and the sign of the divergence changes at $N^{\alpha_2}$, so the extremal sets are, up to lower order, the elements above $N^{\alpha_2}$ that flow down to an element below it. The two streamlined notes (second and third links) prove the asymptotic alone.

Authorship and tools. The full note carries Chojecki alone as author; the two streamlined notes print no author line, the third citing the second as Chojecki's, and none of the three names an AI system. In Chojecki's comment of 15 April 2026 in the discussion thread the author says the first note came out of repeated exchanges with several instances of GPT-5.4 Pro, and the site credits the result to Chojecki and GPT-5.4 Pro. Chojecki's comments of 16 and 17 April 2026 present the Lean development (fourth link) as produced with the Aristotle system: it formalizes the dynamic-programming part of the streamlined argument and leaves two declarations unproved, Mertens' theorem and one analytic estimate, so it is not a complete formal proof.

Third-party formalization. The fifth link is a Lean 4 file in Boris Alexeev's repository, first added on 17 August 2026 and pinned at the commit the formal-conjectures catalog cites. Its header declares it a formalization of a solution to Erdős Problem 858 with informal authors Przemek Chojecki and GPT-5.4 Pro and formal authors Codex and GPT-5.6 Sol, so it is linked here as a formalization of Chojecki's result. Its final theorem erdos_858 states that the largest reciprocal sum over admissible subsets of $\{1,\ldots,N\}$, divided by $\log N$, tends to a constant defined in the file by the same $\alpha_2$ and integral as $c_2$; the file contains no sorry and no axiom, and the catalog's commit of 20 September 2026 reports a rebuild of the file against the catalog's Mathlib with only propext, Classical.choice and Quot.sound as axioms. The formal-conjectures statement file at that commit states the question, marks it research solved, records the result in its docstring, and links this formal proof from its theorem erdos_858 through a formal_proof attribute. This corpus has built neither Lean development, so no formalized evidence is listed and the standing rests on the curator's credit.

Acceptance. The site's curator, Thomas Bloom, marks the problem solved and credits the solution to Chojecki and GPT-5.4 Pro in the problem's remarks, which is the reviewed evidence listed here. Terence Tao's comment of 23 April 2026 in the discussion thread restates the argument as a flow network and gives the same two constants. There is no refereed publication of the result.

Relation to the question. The problem asks for an estimate of $M(N)/\log N$; the result determines its limit, which is the strongest form of an answer the question admits, and the claim value is therefore answered. The earlier results it sharpens are on the problem page.