---

Claim. The answer to Problem 1196 is yes, in the quantitative form: for every real $x\ge2$ and every primitive set $A\subset[x,\infty)$,

$$\sum_{a\in A}\frac{1}{a\log a}\le1+O\!\left(\frac{1}{\log x}\right),$$

which gives the asked bound $1+o(1)$ as $x\to\infty$. Liam Price posted the result in the problem's discussion thread on 13 April 2026 with a written proof on Overleaf and the transcript of the session in which OpenAI's GPT-5.4 Pro produced it in a single run, both linked above; the paper's disclosure cites that transcript as the autonomous run that generated the initial proof. Price, the human submitter, is the claimant. The written account is Boris Alexeev, Kevin Barreto, Yanyang Li, Jared Duker Lichtman, Liam Price, Jibran Iqbal Shah, Quanyu Tang and Terence Tao, Primitive sets and von Mangoldt chains: Erdős Problem #1196 and beyond, arXiv:2605.00301, submitted 1 May 2026, whose Theorem 1.1 is the displayed statement; it is carded at alexeev_2026_primitive_sets_von_mangoldt_chains_erdos, with the statement and the authors' disclosure recorded on its digest. The disclosure says that GPT-5.4 Pro generated the initial proof, that the human authors contributed to and reviewed the final proofs, and that the Lean formalizations were produced with Codex and with Math Inc.'s Gauss. The method, Markov chains with von Mangoldt weights in the words of the paper's abstract, runs, as the thread describes it in detail, a Markov chain downward on the divisibility order, stepping from $n$ to $n/q$ with probability $\Lambda(q)/\log n$, which the identity $\sum_{q\mid n}\Lambda(q) =\log n$ makes a probability law; a chain started above $x$ meets a primitive set at most once, and Mertens's theorem turns the total mass into $1+O(1/\log x)$. The thread also carries sharpenings of the secondary term: Terence Tao's bound $1+2\gamma/\log x+O(1/\log^{2}x)$ from the canonical measure, a thread post which the paper's Remark 4.2 gives as an alternate proof, and Nat Sothanaphan's dated notes, which sharpen the bound to $1+\gamma/\log x+O(1/\log^{2}x)$ and give a pure resummation proof, recorded on [[problems/divisors/E1196/claims/2026_04_16_sothanaphan|Sothanaphan's page]].

Submission note. Posted to the site's forum by Liam Price on 13 April 2026:

GPT-5.4 Pro claims a solution here.

You can also find the 5.4 Pro chat that solved the problem here.

Depends on. No page of this wiki.

Acceptance. Thomas Bloom, the site's curator, labels the problem proved and credits the solution to GPT-5.4 Pro prompted by Price, with the paper as its account, on the problem page, last edited 12 May 2026; that credit is the reviewed evidence. The paper is an arXiv preprint with no journal record, so no refereed evidence is listed.

Formalization. The thread reported on 16 April 2026 that Math Inc. had formalized the solution in Lean; the paper's reference names the repository Erdos1196 and the commit the link above pins, and cites it as a formalization of a version of Theorem 1.1. The site's label notes this Lean development. An earlier Lean attempt reported in the thread on 14 April 2026, generated by Aristotle from Price's write-up, left three lemmas unproved and is not a formalization of the result. A thread post of 21 June 2026 links a single-file copy of a Lean proof in a catalog repository of such files; the file names no informal or formal author and declares no result it formalizes, so it is not linked. This corpus has not built or audited any of these developments, so no formalized evidence is listed.

What remains. Nothing of the question. Lichtman's earlier bound $e^{\gamma}\pi/4+o(1)$ on Lichtman's card is superseded; the case $x=1$ is Problem 164.