---

Claim. Let $F(n)$ be the largest size of a set $A\subseteq\{1,\ldots,n\}$ such that $a\nmid bc$ whenever $a,b,c\in A$ with $a\ne b$ and $a\ne c$, the case $b=c$ included, which the manuscript calls strongly 2-primitive and which is the site's condition. Theorem 1.1 states that, as $n\to\infty$,

$$F(n)=\pi(n)+\Bigl(\frac{27}{2}+o(1)\Bigr)\frac{n^{2/3}}{(\log n)^2},$$

so the constant $C$ the problem asks for exists and equals $27/2$. The source is P. Chojecki, The second term for strongly 2-primitive sets, a five-page manuscript served by the author's organization (PDF metadata dated 13 July 2026, posted in the site's thread the same day), with the result page Theorem 1.1 on the source card. The upper bound (Proposition 2.4) follows Erdős's 1938 argument: every integer up to $n$ is a product of two members of a basis made of four classes (the integers up to $n^{3/5}$, the primes in $(n^{3/5},n]$, the products $pq$ of two primes up to $n^{1/3}$, and the products $qr$ of primes $q$ and $r$ with $n^{1/3}<q\le n^{2/5}$ and $r\le n/q^2$), a strongly 2-primitive set has at most as many members as the basis, and the prime number theorem with partial summation gives the counts $(9/2+o(1))S$ and $(9+o(1))S$ of the last two classes, $S=n^{2/3}/(\log n)^2$. The lower bound (Proposition 3.4) packs a linear family of prime triples with products at most $n$, built from proper edge-colorings between logarithmic bins of primes near $n^{1/3}$, and takes the unused primes together with the triple products; the cell weights sum to $(27/2-o(1))S$.

Provenance. The manuscript's byline footnote declares AI assistance in exploring the argument and writing the text, and the site's commentary attributes the proof to GPT 5.6 Sol prompted by the author; the manuscript names one human author, who is the claimant.

Acceptance. Reviewed: the site's curator, Thomas Bloom, who neither submitted nor co-wrote the claim, labels the problem PROVED (LEAN) with the page last edited 14 July 2026, and the curator's commentary credits the asymptotic to GPT 5.6 Sol prompted by Chojecki, with the manuscript linked; the curator's thread comment of 14 July 2026 states that the upper-bound proof is Erdős's own 1938 argument with its constant tracked and that the lower bound is the same construction as Erdős's, reduced to a linear 3-uniform hypergraph on primes; the page as accessed 2026-09-18 and 2026-10-07 shows thirteen comments, one proof claim and no exposition. Not refereed: the manuscript was posted to arXiv on 14 July 2026 (arXiv:2607.15306, one version, same title and author; record read 2026-10-02), which is not refereeing, and no journal version or written expert review of the manuscript was found (Crossref bibliographic query of 2026-09-18 recorded on the problem page). Not formalized here: two Lean developments are linked, and neither is counted as formalized. The development the thread names, ErdosProblem793.lean in van Doorn's public repository, linked at the repository's head of 10 September 2026, proves the asymptotic from the prime number theorem declared as its one axiom; it is not built or audited in this repository. The formal-conjectures collection held no statement of the problem on 18 September 2026 and added ErdosProblems/793.lean on 19 September 2026; at that commit, its variant stating the constant $27/2$ carries a formal-proof attribute naming the file Erdos793.lean in Boris Alexeev's repository plby/lean-proofs, linked above at the pinned commit. That file declares itself a formalization of this manuscript's result, naming GPT-5.6 Sol Ultra prompted by Chojecki as the informal authors and Aristotle and Wouter van Doorn as the formal authors; it is a port of van Doorn's development that draws the prime number theorem from the PrimeNumberTheoremAnd project in place of the axiom and records in a comment that its theorem depends only on the three standard axioms. Because it declares itself a formalization of the claimant's result, it is a link on this page and not a claim of its own; it was not built or audited here. The site's "(Lean)" suffix is its catalog label. The problem page records the manuscript's eight named statements read for their claims, with no step checked here; this page rests on no review of its own.

Scope. Full for the site's statement. The proof-claim tab holds a proof claim of 5 August 2026, to which the site gives no kind; its Lean file proves for every $k\ge2$, $k=2$ included, that the constant exists, without evaluating it: van Doorn 2026. The convention requiring $b\ne c$ defines a possibly different function, which the theorem as stated does not address; van Doorn's file proves the same constant $\Lambda_3$ for both conventions.

Depends on. No page of this wiki.