---

Claim. In the game of Problem 872, two players alternately pick unpicked integers from $\{2,\ldots,n\}$ so that no picked integer divides another, until no legal pick remains; Prolonger, who moves first, wants many picks and Shortener wants few. Let $L(n)$ be the value of this finite game, the number of picks Prolonger can force. The claim is

$$L(n)=o(n),$$

so for no $\epsilon>0$ does the game last $\epsilon n$ moves for all large $n$, and both displayed questions have the answer no. This is the theorem of Om Buddhdev's manuscript Erdős Problem 872: the divisor-antichain game has o(n) guaranteed length (Zenodo record of 24 July 2026, version R179, DOI 10.5281/zenodo.21545919, CC BY 4.0). On the thread the author adds that the same conclusion holds when Shortener moves first; the manuscript fixes Prolonger first.

Submission note. Posted to erdosproblems.com as a proof claim by Om Buddhdev (account Om_Buddhdev_sensho) on 30 July 2026, giving "Fable 5, GPT 5.6 Pro, and some others over ~400 prompts and 3mo (noted in writeup)" as the AI used:

Write $L(n)$ for the guaranteed game length, claiming $L(n)=o(n)$ with the answer "no" to both questions. Since a mid-game position is not a smaller copy of the game, we dominate $L(n)$ by a padded variant $V_b(n)$, the maximizer gets $b$ free opening moves, may pass, and an ally may erase any up-set, chosen so that restricting to multiples of $t$ and dividing out $t$ gives the same kind of game. Factor each $x=at$ into a smooth part $a$ and a rough part $t$. A Selberg-sieve estimate shows that off a set of arbitrarily small density, $P^-(t)>Hn/t$ with $H>1$; two such rough parts with $\mathrm{lcm}\le n$ must then divide one another, so the minimal ones partition almost all of $\{2,\dots,n\}$ into blocks, each a copy of the variant on a board of size $o(n)$ with one extra opening move. A sweep-and-pairing strategy confines the maximizer to blocks of at most half the total weight, so $c_b\le\tfrac12 c_{b+1}$ where $c_b=\limsup V_b(n)/n$; since $c_b\le1$, $c_1=0$. Notes: Sorry, I don't have an arXiv endorsement, so the writeup is on Zenodo. I hope that suffices. Technically it is not yet completely formalized in lean, all of the game-theoretic content is kernel-checked. One analytic input, Lemma 2.3, a sieåve estimate, taken as the axiom A3_exceptional_set_estimate, is proved in the manuscript and not yet formalized. Adversarial audits of the proof have so far found nothing wrong with it. I'll update the thread once it is completely formalized.

Argument. Because a position reached in play is not a smaller copy of the game, the manuscript bounds $L(n)$ by the value $V_b(N)$ of a robust variant on divisibility downsets of $\{1,\ldots,N\}$: Prolonger gets up to $b$ opening moves and may later pass, and an ally may before any move erase any divisibility upset; $L(n)\le V_1(n)$. Writing $c_b$ for the upper limit of $V_b(N)/N$, the proof shows $c_b\le\tfrac12c_{b+1}$, and since $c_b\le1$ for all $b$ this forces $c_1=0$. For the recursion each integer is factored into a smooth part and a rough tag $t$; a sieve estimate (the manuscript's Lemma 2.3) shows that outside a set of arbitrarily small density the tags are so rough that the cones $t\{1,\ldots,\lfloor n/t\rfloor\}$ of minimal tags are disjoint and cover almost everything. Shortener sweeps the roots of these cones; each cone that Prolonger activates is a copy of the variant on a board of size $o(n)$ with one more opening move, so an adaptive pairing confines Prolonger to cones carrying at most half the total weight. The author says on the thread that the argument fixes parameters and diagonalizes, so it gives no explicit rate.

Covers. The two displayed questions, both answered in the negative: the game cannot be guaranteed to last $\epsilon n$ moves for any fixed $\epsilon>0$, nor $(1-\epsilon)n/2$ moves (the second also claimed, with Prolonger first, by the pending partial claim [[problems/divisors/E0872/claims/2026_02_14_price|Price's Shortener strategy]]). The order of $L(n)$, the problem's headline question, is not determined: the manuscript gives no rate, and the author agreed on the thread that how long the game lasts remains open, describing the result as a full solution to two of the three questions. The forum lists the claim as a full proof claim.

Formal verification by the author. The folder linked above holds a Lean 4.28.0 project whose theorem Erdos872.main states that the ratio of the original game's value to $n$ tends to $0$. At the time of the claim the manuscript reported about 12,000 lines with no sorry, resting on one problem-specific axiom, A3_exceptional_set_estimate, the sieve estimate of Lemma 2.3, which was proved in prose and not in Lean. Later on 2026-07-30 the author reported on the thread that the formalization was complete, and the folder's report of that date records a Lean proof of the estimate in six new modules (1,524 lines, with a factorial-period sieve in place of the manuscript's Selberg weights), a rebuild of all 42 targets, the deletion of two unused analytic axioms, and the axiom report propext, Classical.choice and Quot.sound for Erdos872.main. The link pins the commit of that report. None of this has been built or audited here, so no formalized evidence is listed; the formal-conjectures statement file of the problem, which also fixes Prolonger first, is a statement and not a proof.

Claimant and systems. Om Buddhdev, posting under the forum account Om_Buddhdev_sensho, submitted the claim on 2026-07-30 and signs the manuscript alone. The forum's tab names Fable 5, GPT 5.6 Pro and other systems over about 400 prompts and three months; the manuscript says it was produced by an AI research system, GPT-5.4, GPT-5.5 and GPT-5.6 Pro as primary researchers and Claude Opus 4.8 and Claude Fable 5 as curator-researchers, directed by the author between April and July 2026, with the research record in the linked repository. The author's earlier manuscript of April 2026, announced on the problem's discussion thread, gave $L(n)<0.19n$, the unconditional lower bound $L(n)\ge(\tfrac18-o(1))n\log\log n/\log n$, and a lower bound of order $n(\log\log n)^2/\log n$ conditional on a restricted safe-edge hypothesis; the present result supersedes its upper bound. A finite $K_5$ computation reported by Edwin Rosero refuted that hypothesis, and on 12 July 2026 the author posted a note and a revised manuscript claiming $L(n)\ge c_\delta n(\log\log n)^2/\log n$ for every fixed $0<\delta<1/4$ without it, unreviewed and with its two new selector arguments not formalized in Lean.

Standing. Posted on the problem's forum on 2026-07-30 with the Zenodo record and the Lean folder as its external links; the author notes there that the write-up is on Zenodo for want of an arXiv endorsement. On 2026-10-07 the claim carried four comments, between a forum commenter and the author: the bound gives no explicit rate and would be far weaker than the lower bounds if made effective; the author agreed that the order of $L(n)$ remains open; and the author stated that the result does not depend on who moves first. The site's curator has not commented, the site labels the problem OPEN (page last edited 24 April 2026), no refereed publication exists and nobody has recorded accepting the result, so the claim is claimed.