Erdős Problem 872: the divisor-antichain game has o(n) guaranteed length

Two players, Prolonger and Shortener, alternately select integers from {2,…,n}, with Prolonger moving first, so that the selected set remains an antichain under divisibility. Prolonger maximizes the total number of selections and Shortener minimizes it. Writing L(n) for the value of this game, we prove L(n) = o(n): the game cannot be guaranteed to last εn moves for any fixed ε > 0, answering the displayed questions of Erdős Problem 872 in the negative. The proof passes to a robust envelope game with adversarial erasure, decomposes the board by a K-dense/rough-tag factorization, establishes a laminar structure of disjoint root cones, and analyzes an adaptive sweep strategy for Shortener, yielding the density recursion c_b ≤ ½·c_{b+1} and hence c_1 = 0. The argument is formalized in Lean 4 (theorem Erdos872.main, ~12,000 lines, no sorry): the statement for the original game is kernel-checked from exactly one problem-specific axiom, A3_exceptional_set_estimate — Lemma 2.3, an exceptional-set density estimate proved in the manuscript by the Selberg sieve and Rankin's method but not yet formalized. Axiom report: propext, Classical.choice, A3_exceptional_set_estimate, Quot.sound. 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, with an independent Lean kernel check — directed by the author over roughly three months (April–July 2026). Complete research record: https://github.com/xa8zz/erdos-harness