#181: OpenAI's proof that R(Q_n) = O(2ⁿ) — 172 pages read by nine hostile seats, sources checked, and a third-party Lean 4 kernel check replayed on our own machine

The problem (erdosproblems.com/181; community database status OPEN as of our 11 October refresh). Let Q_n be the n-dimensional hypercube graph (2ⁿ vertices, n2ⁿ⁻¹ edges). Prove that R(Q_n) ≪ 2ⁿ. Burr and Erdős raised it in 1975 as the sharpest test of their conjecture that bounded-arboricity families have linear Ramsey numbers: the cube has n/2 = ½log₂|V| edges per vertex, the largest density their own first-moment bound permits a linear family to have. The lower bound is 3·2ⁿ⁻¹ − 1 (two red blocks, blue between). Upper bounds: Graham–Rödl–Ruciński 2001 gave 8(16n)ⁿ; Shi (2001, 2007) made it polynomial in 2ⁿ; Fox–Sudakov n·2²ⁿ⁺⁵; Conlon–Fox–Sudakov 2²ⁿ⁺⁶; Lee's degenerate-graphs theorem (Annals 2017) (1+o(1))2²ⁿ; and Tikhomirov (2022, EJC 2024) 2^2n−cn+1 + 2 with c ≈ 0.0366 — the first exponent below 2. Our own July working report audited that literature and re-verified a finite case; it did not touch the asymptotic question.

What OpenAI claims. The hypercube Ramsey number has linear order (23 September 2026, family 171 of the 6 October release, 172 pages, no Lean in the release). Theorem 1.1: there is an absolute constant C with R(Q_n) ≤ C·2ⁿ for every n ≥ 0 — the conjecture exactly, with no numerical value for C and, the paper says plainly, no information about whether R(Q_n)/2ⁿ converges.

How the proof is built (plain version). It is a proof by contradiction along a sequence. If the ratio R(Q_n)/2ⁿ is unbounded, Lemma 2.1 produces dimensions n → ∞ and two-colourings between two disjoint host sides of size N each, with no monochromatic cube across the sides, N ≤ n2ⁿ and C_n = N/2ⁿ → ∞ at no prescribed rate. Everything after that is "eventually along this sequence". Lemma 3.2 is the compactness engine: for any countable list of patch properties, pass to a subsequence and throw away o(N) labels so that each property is either eventually absent or available — survives every removal of a fixed fraction κN of labels. The first twelve sections prove discrepancy: every pair of probability laws on the two sides, within the width budgets in play (width = log of N times the largest atom), sees edge density within a vanishing error of ½ in both colours — because any available bias, purity, polynomial density cap, small-grid purity, asymmetric purity, intermediate bias exponent, full-dimensional cluster or "linear-budget jump" is shown to yield a monochromatic cube directly (Sections 4–11), each construction paying its local repetitions and predictive tests out of the density surplus it assumes. Section 13 then extracts disjoint host patches of one colour, one orientation and one of finitely many modes, and allocates the cube to them as subcubes fixed by initial coordinates with dyadic weights rounded from the patch masses (Kraft equality makes the prefix code exact; the retained patches carry more than half the mass; each role has ℓ_i "crossing" edges into other patches, with ℓ_i and log(N/M_i) both charged to the patch's gain budget s_i/(1000u)). The gain is the (M/N)(1+2δ)ⁿ story from §1.3: n independent restrictions that each keep a label with probability ½+δ leave M(½+δ)ⁿ labels, so a density surplus can pay for a smaller support. When the surplus is large (Section 15) the odd roles are assigned injectively and the even roles get weights supported on their common neighbourhoods whose column sums are O(1/C_n); Hall's theorem does the rest. When the surplus is small or zero (Sections 16–18, including the bounded case of one patch of size ≍ N with no gain at all) a fixed linear map on cube words sorts the odd roles into syndrome classes — the coordinate IDs are distinct, so an even role has at most one neighbour in each class — and O(log n) late classes get provisional labels that are replaced one class at a time from reserved host sets; each even role ends with two random candidates adjacent to all its assigned neighbours, and Hall fails only when the multigraph on labels with one edge per even role has a connected component with more edges than vertices. That is where the "no rate" promise is cashed: the expected number of such components is bounded by e^O(r)·M·(K/C_n)^ηn plus a convergent small-set sum, and n·log 2 + ηn·log(K/C_n) → −∞ "however slowly C_n → ∞" once C_n exceeds a fixed constant.

What we checked ourselves before the seats reported: Lemma 3.2's dichotomy with its quantifiers written out (the negation of "available" is an infinitely-often statement, and the proof applies the dichotomy member by member, which is what makes "an available finite union has an available member" sound); Lemma 3.7, the gated posterior comparison, which is a two-line Bayes bound once the selection event is inside the likelihood; the dyadic allocation of §13.2 (the first segment of decreasing dyadic weights to reach 1 reaches it exactly, and Σ_J M_i > S/2 because each weight is below twice its mass); the endpoint-multigraph count of §18.5 (a connected Hall-violating p-set needs two mergers beyond its spanning tree; integrating leaves at K/M each and the two surplus edges at M⁻²e^.01n gives K^pM^−p−1e^.02n, as printed); the §15 union bound N·(K′/C_n)ⁿ = o(1), which uses N ≤ n2ⁿ and nothing about the rate of C_n; and Lemma 16.1's syndrome classes. None of this is a check of the 150 pages in between — that is what the seats were for.

The paper as written — a nine-seat hostile read. We refereed the 172-page preprint the way we refereed OpenAI's Hindman paper for #172, scaled to its length: seven tool-equipped Opus seats with disjoint scopes over the mathematics (§2–3 the probabilistic framework; §4–5; §6–7 through the first discrepancy milestone (7.2); §8–9; §10–12; §13–15; §16–18 and the final matching), one over the bibliography and the live world, and one over the Lean source — each briefed that the base rate for a machine-written 172-page proof of a famous conjecture being correct is low, that its job was to find the sentence where it fails, to fetch every cited theorem from its current source rather than from memory, to track every constant's dependencies, to hunt for any hidden rate on N/2ⁿ → ∞, and to say which steps it verified line by line and which it only skimmed. Every objection below carries its quote in the bundle; the seats' own lists of what they skimmed are the honest edge of this read.

§2–3, the framework (seat: framework) — HOLDS AS READ. Lemma 2.1 loses nothing (no later section uses an edge inside a host side; N ≤ n2ⁿ is used only for unions over e^O(n) labels). Lemma 3.2's dichotomy is exact: "not available" is precisely liminf τ_n/N = 0, i.e. eliminable by o(N) removals along a subsequence; the diagonal choice keeps total removals ≤ N/j; the finite-union clause is correct when read as "available along no subsequence" (the seat wrote a cleaner pigeonhole proof); every later invocation runs over countably many rational parameters. Lemma 3.3's K = 4/κ depends on the counterexample sequence, not on nothing — and at every use checked it only multiplies negative powers of n or terms beaten by C_n → ∞, so no circularity. Lemmas 3.5–3.10 re-derived; 35+ later invocations spot-checked against their hypotheses, the §4 uses of 3.6–3.9 line by line including the recomputation of selection inside the likelihood. One lead was run to ground: the formalizers' design note records that their first decomposition of Lemma 3.9 (calibrated near-product injections) was false — it claimed every completed atom is at most 10/d, when only the dummy atoms are O(1/d), and it took an existential "some injection law has additive singleton error" that cyclic shifts satisfy while breaking (3.2). The paper's text avoids both traps: it says only the dummy rows' atoms are O(1/d), proves the joint bound for one specific sequential sampler conditioned on its tracking event, and gets exact marginals by separation inside the set of laws satisfying the joint bounds. Exposition notes: Lemma 3.8 is stated in n but §14 applies it to an internal dimension h that may stay bounded (valid — the thresholds depend only on fixed parameters and Q₀ is chosen after them — but unsaid). Fetched and matching: Erdős–Lovász §2, Lu–Székely Lemma 3, Lipschitz percolation, dependent rounding (P1)–(P3), Hoeffding, Azuma, Freedman. Not fully checked: the ball-intersection exponent in Lemma 3.8 Step 3, the branching domination in Lemma 3.10 Step 5, the mesh-limit argument's constants.

§4–5 (seat: initial_a) — HOLDS AS READ, no gap of either kind. Lemma 4.1 re-derived from the rendered pages: plateau and trimming, the coordinate-key gadget, validity of tuple sets with the Azuma dip count, marking and height choices, the posterior bound |S| ≥ N·e^{−(log 2 − c₂a*/2)n}, mask balancing via Kakutani, the Hall step. Selection is recomputed as the tuple varies (the gate reads only preparatory data; the reference law deletes the whole tuple). Lemma 5.1 checked through every displayed estimate — the parent/stream construction with a₀ = 1/3, prefix-deletion and block-reconstruction tests, the odd-row comparison P ≤ e^a₃kQ_c, the minimax common high-row law, the selection correction for low rows, F_z ≤ e^a₆knQ, the posterior density e^τ₀kn, the even-row cap O(e^τ₁n), three-level odd column sums, the clock-lemma interface, Hall. Two corrections to our own brief: §5.4 is not a Kakutani application but Markov plus the local lemma in five stages; and τ₁ < log 2 is not the operative condition — what is needed is τ₁ < log 2 − H_bin(2ρ) acting on the repeat term of the scattered-moment bound, with ρ chosen after τ₁, no cycle. Constant order q₀ → a_i, δ → K_h, η → K₁ → K₂ → K₀ → K_D → K_s → K_B → α → height exponents; none depends on n, the witness or the removed sets. Minor: Lemma 4.1 uses "bad sequence" and "current sets" without defining them; log q ≥ −log 2 + .7a_i stated without proof (true for a_i ≤ ½); §5.4 Stage 4 justifies a product over J → ∞ variables by "(1+o(1)) per variable", which is not enough as written though the product is e^o(s) — the one place where the stated reason is not the real one; the observation-record counts on p. 39 asserted, not derived. No rate on C_n: it enters only through |A|/N, |B|/N → 0.

§6–7 and the first milestone (seat: initial_b) — HOLDS AS READ. (7.2) is reached by stabilizing three fixed properties in order: a violation of (7.1) would, by Lemma 3.3 and Lemma 6.1 with the sides swapped (γ = ¼, p₀ = c/2), give a cube, so it is eventually absent; purity at widths 2n^d/4 with defect ≤ e^−nh would, by Lemma 7.1 with p = h/2, contradict (7.1); with purity absent, Lemma 4.1 excludes bias at widths n^d/4. So η₀ = h = d/(4·10⁹), an absolute constant: D* → D₀ → d → (b, c, h) → η₀ with no cycle, D* genuinely universal (it enters only through η ≤ n^2D*Λ with 2D* < d₀, and d₀ depends on nothing in the inputs). Re-derived: e^.4kn, O(e^.55n), n^d/2 + 2cn^d log n, .04n^4d; Lemma 7.1 Steps 1–6; Lemma 6.1 Steps 1–3 with the three-stage conditioning, the marking/maximality argument and both load cancellations; the selection bias handled three different ways for even rows, low odd rows and high odd rows. Lemma 3.2 is applied here to a list of three fixed properties, so countability never arises. Cosmetic: the swapped Lemma 6.1 is never stated; two O(1) caps are really O(K); no tie-break in the marking rule; Lemma 3.9 applied "with d = N" when the retained side is smaller (pad with zero-mass labels); d not declared rational. Unclear only by dependency: the §6.2 descriptor counts rest on §5.3's state geometry.

§8–9, asymmetric widths and the intermediate bias exponents (seat: asymmetric) — HOLDS AS READ, with one step the seat could not check line by line. All twelve steps of Lemma 8.1, Corollary 8.2, Definition 9.1, the parameter selection of Proposition 9.2, §9.2 (core erasure, the covariance tail, the Finner/Hoeffding concentration) and §9.3 re-derived. "No relation p > τ is required" is correct — every use of p needs only e^−np/2·poly(n) → 0. Corollary 8.2's list of width pairs is countable (rational pairs, the exponent a function of the pair), so Lemma 3.2 applies, and the one downstream use needs one pair. H^† and H_L^† are well-defined monotone limits in [0, ∞]; the case split is exhaustive, with H^† = 1, H_L^† = 1, H^† = ∞ and H^† = 0 all covered and nothing concluded at an infimum. Separate dependency graphs for the two cases of Proposition 9.2 — the appendix warns they use different parameter orders — have no cycle and no constant depending on n. Selection is recomputed where the hidden tuple varies (§8 Steps 6–7); in §9 the center map is fixed in advance, so there is nothing to recompute. Finner's inequality fetched from Project Euclid and matching (its §3 allows Σ1/p_j ≤ 1 on probability spaces, the form used). No rate on C_n. The unchecked step, §9.1 (pp. 81–82), UNCLEAR: the map assigning each cube position to a nearby center is built by "adapting Steps 2–4 of Lemma 3.8", but Lemma 3.8's stated hypotheses do not cover this case — the radius n^σ is not one the lemma allows (fitting it to the small-radius option would need b > 2.97 where the lemma requires b < 1), the paths cross slices and the crowd tests are replaced by three new ones, and the Lipschitz step (Step 5) is used but not mentioned. Every exponent condition the sketch states was checked and none fails (base case, overlap estimate, the ratio χ/2 > a + 4σ_h, configuration count, the union over 2ⁿ sites); the induction itself is two paragraphs of sketch, and the construction is genuinely needed — simpler coverings give too many centers for the width budget. An exposition gap rather than a known mathematical one; it is the one place in the proof where a referee has to take "the same argument" on trust. Minor: "we call these the base gates" in §8 can be read as excluding the η_g, Z_g bounds Step 4 needs; §9.3 reuses one constant c for two roles where the charge constant must be strictly smaller; Lemma 3.10 applied without stating B (B ≥ 2 is needed; §8 uses 3); ρ and σ clash with Lemma 3.8's symbols.

§10–12, cluster exclusion, the linear-budget jump and deep discrepancy (seat: cluster) — HOLDS AS READ. Every displayed inequality on pp. 89–111 re-derived, the borderline arithmetic checked numerically: Proposition 10.1's list test (10.1), eligibility rule, tilt tails, the e^.1m mean cap and the likelihood bound (10.2), the posterior and "light part" step, column-sum concentration, and the clock-lemma and Lemma 3.6 hypotheses; Corollary 10.2 including its second use in Lemma 13.2 (a valid rational δ exists because a_C < min(η₀,1)/10⁶); the §11 slice experiment, Lemmas 11.2 (Kakutani's closed graph checked) and 11.3, §11.3, Corollaries 11.4 and 12.1; Lemmas 12.2–12.6 in full; Appendix A's rows and Figure 1 agree with the text and the dependency order has no cycle. The reverse-orientation discrepancy n^−.95 that Proposition 11.1 needs comes from neither Corollary 8.2 nor 12.1 but from the case hypothesis H^† ≥ 1 in the reversed orientation via Definition 9.1 — not circular. The sharpest budgets hold with margin: n·b_* = n^.05 ≪ gh = n^.09, and the deep error n^−.96 needs b_* = o(n^−.94) and b_* < n^−.905. Selection is recomputed when the hidden tuple varies, in L_w (p. 94) and F_w (p. 98). No rate on C_n. Thirteen exposition objections, two of which matter: on p. 93 the supremum defining w_ℓ,c must be read as over eligibility sets of size ≥ .99λ — under Lemma 3.8's generic ≥ λ/3 reading the per-slice sum becomes 3 and the claimed bound N·max p̂_b ≤ e^.1m fails; the text supports the .99λ reading, so the claim holds as intended, but a reader who takes the lemma's own constant will think it broken. And on pp. 92 and 96 the independence of well-separated roles rests on a "primitive domain" locality claim whose distance arithmetic checks but whose measurability is asserted rather than proved — the one structural point in this scope worth confirming against the Lean. Hamming 1950 §3 (archive.org scan) and Azuma's Remark 1 fetched and matching.

§13–15, allocation and the high modes (seat: allocation) — HOLDS AS READ. All of §13 checked: the cluster witness Lemma 13.2 builds really is a Corollary 10.2 witness; fixing one colour and one orientation is a pigeonhole over twenty types at each n — and necessary, since the host is bipartite and every patch must send odd roles to the same side; the dyadic rounding is as we read it; crossing edges go to distinct leaves and are crossings from both ends, matching Conlon–Fox–Lee–Sudakov's Proposition 2.2(ii) (fetched); labels in different patches are distinct because the patches are; the N/3 reserve is set aside before extraction and used only in §16; the budget ℓ_i, log(N/M_i) ≤ s_i/(1000u) holds for every retained patch, with the size constant c independent of Q₀, which it needs to be; Lemma 13.4's three degree windows, clique exclusion and mesh stability check. §14: (14.1), the likelihood bound, the cap N·max σ_v ≤ 2^he^−500s, the mean bound Eσ_v ≤ K/M_i, Kakutani's hypotheses in Proposition 14.2 and max π_i ≤ 11/M_i at the fixed point all re-derived; fixed low-mode scales are fine inside §14 because the estimates only need scales above Q₀. §15: Lemma 15.1 in full including the clock lemma with B = 5 and the union bound N(K′/C_n)ⁿ → 0; both cluster-history alarms; Lemma 15.2; the small/large-bin scale relations; and the Hall step — odd labels injective across patches, even rows supported on common neighbours of all odd neighbours including crossings, normalization preserving column sums ≤ 1. Two UNCLEAR, both exposition: in Proposition 15.4 the order of comparisons and reverse integration for small-bin repeats is asserted rather than derived (every cost exponent checks); in Proposition 15.3 the seat did not confirm that the certificate events' dependency graph is exactly the one Lemma 3.5 requires. No rate on C_n: the high modes need C_n above an absolute constant and N ≤ n2ⁿ.

§16–18, the low modes and the final matching (seat: lowmodes) — HOLDS AS READ, with one exposition gap. Lemma 16.1 by hand: the syndrome map, class sizes 2ⁿ⁻¹/H_*, at most one neighbour per class, at least ⌊j/2⌋ neighbours in the last j classes, at most one late internal neighbour. Lemmas 17.1–17.3 and Proposition 17.4 hold; the polynomial slack of the bounded regime comes from deferring the p(v) ≥ A₀log n/2 late hits (Lemma 17.1). Injectivity: early labels sit in disjoint cells and patches outside the reserve, late labels come from disjoint late pools, injective within each class. Adjacency: each even role's two candidates hit every odd neighbour — internal, bulk, crossing, and late after replacement. Lemma 18.6 as we read it: tree diagrams give p+1 classes, a violator needs two further merges with two edges at the maximum weight, both sums vanish. Every occurrence of C_n in §16–18 traced: the facts used are C_n → ∞, N ≥ 2ⁿ, N ≤ n2ⁿ — no rate. The gap, Lemma 18.1 (p. 149): the proof says "For a target sketch, its empirical hit fraction H(y) … has mean .5 + O(b_*). In its second moment, nonconflicting pairs contribute .25 + O(b_*) by (18.2)" — but (18.2) covers only labels in D_v⁰ and nonconflicting pairs there, and the lemma's hypotheses never say the sketch entries lie in D_w⁰. As worded for arbitrary side data the implication is false: the formalizers built a finite model satisfying both requirements with zero retained mass, and the seat checked it. The missing premise — every sketch entry lies in D_w⁰ — holds automatically on the paper's own gate (the sketch is drawn from τ_w^j, supported in D_w⁰ unless the fallback point mass is used, which the gate rules out; a fallback sketch would also break Requirement 1 by itself), and the paper states the support condition explicitly in the parallel spot in Lemma 18.2. Two seats reached this independently — the Lean source audit found the formalizers' record of it, and the §18 seat confirmed it from the text. The conclusion is true; the wording is incomplete. That is the only gap of any kind in the proof that this read found. Cosmetic: Proposition 18.4 applies the clock lemma with its dimension parameter replaced by e^nδ′ without the lemma saying its parameter is arbitrary; Proposition 16.3 imports §15.2's capacity certificates at target .2 without redoing the constants (not fully checked). Moser–Tardos, Haeupler–Saha–Srinivasan Theorem 2.2, Harris–Srinivasan, Lu–Székely all fetched and matching.

The bibliography and the live world (seat: citations) — ACCURATE. All 34 references exist; all 31 DOIs resolve and Crossref or zbMATH matches every author list, title, venue, volume, issue and page range; both renyi.hu links serve the right Erdős scans; the LaTeX source carries the same 34 entries in the same order. Every theorem-number citation in §1.1–1.2 was read in its source and quoted beside the paper's paraphrase: Burr–Erdős's L-set definition in §1, Lemma 3.3, Lemma 4.3 and the §7 cube question; Graham–Rödl–Ruciński's Theorem 1 with its strict inequality; Fox–Sudakov Corollary 1.3 and Lemmas 2.1–2.2; Conlon–Fox–Sudakov Corollary 4.2 and §4; Lee's Theorem 1.3 and the paragraph after it giving 2²ⁿ + n²2ⁿ; Tikhomirov's Theorem 1.1 and Corollary 1.2; Gowers §4 Lemma 11; Sudakov §2; Kostochka–Rödl Lemma 1; the main theorems of Conlon–Fox–Lee–Sudakov, both Fiz Pontiveros–Griffiths–Morris–Saxton–Skokan papers and Mota–Sárközy–Schacht–Taraz. Chvátal–Rödl– Szemerédi–Trotter, Beck and Shi 2007 could be checked only through secondary sources, which agree. The paper's own small arguments are right: the 3·2ⁿ⁻¹ − 1 two-block lower bound, the reflected Gray code (checked by script for d ≤ 8 with a negative control), the F^□k ⊆ Q_dk embedding. Known exact values are R(Q₂) = 6 and R(Q₃) = 13 (Lidický–Pfender 2021); no published bound on R(Q₄). Four cosmetic notes: "[3, Section 3]" needs §1 as well; Tikhomirov's Corollary 1.2 exists only from arXiv v3 (2 March 2024) on; "Sudakov explicitly drew on Gowers" overstates Sudakov's "was influenced by"; an orphan source file 01-regime-guide.tex never reaches the PDF. No fabricated bibliographic detail anywhere.

Novelty. No human proof of R(Q_n) = O(2ⁿ) and no improvement on Tikhomirov anywhere we could look (arXiv sweeps, the Erdős-problems site and forum, Tao's post, MathOverflow, Hacker News, Mathstodon, press). The preprint is not on arXiv; it was never revised after its 6 October commit; openai/math has issues and discussions turned off, so no public correction can be filed there. OpenAI's own Lean library proves 2ⁿ ≤ R(Q_n) ≤ 4²ⁿ and the Lemma 2.1 reduction, nothing more. erdosproblems.com/181 shows no status and does not mention OpenAI; Bloom's 8 October post lists the claim as "not formalised" under his blanket disclaimer; the teorth database still says OPEN and unformalized; no comment from Tao, Conlon, Fox, Sudakov, Tikhomirov or Lee.

Verdict on the paper as written: HOLDS AS READ, nine seats out of nine; no mathematical gap found. What the read did find, in order of weight: one exposition gap (Lemma 18.1's second-moment step needs a support premise the lemma's wording omits and the gate supplies — found independently by the §18 seat and, through the formalizers' own notes, by the Lean seat); one step taken on trust (§9.1's center map, "adapting Steps 2–4 of Lemma 3.8" outside that lemma's stated hypotheses — every exponent condition checks, the induction is a sketch); one reading that is load-bearing (p. 93's supremum must be over ≥ .99λ eligibility sets, which the text supports and Lemma 3.8's own constant would not); one asserted measurability (pp. 92, 96); two compressed orderings in §15; a "(1+o(1)) per variable" in §5.4 that is not the real reason the product is small; and a few dozen cosmetic notes — undefined terms in Lemma 4.1, reused symbols, lemmas applied to parameters they were not stated for (Lemma 3.8 on an internal dimension h, the clock lemma with an exponential dimension), unstated tie-breaks and B values. Every one of these has its quote in the bundle, and every one, where the seat could decide, resolved in the paper's favour. The one place every seat was told to hunt — a hidden rate on N/2ⁿ → ∞ — came back empty nine times: the only facts used are C_n → ∞, N ≥ 2ⁿ and N ≤ n2ⁿ, and every threshold on C_n is a fixed constant. What this is not: a human expert's reading, or a check of every constant — the seats' skimmed lists (Lemma 3.8 Step 3's exponent, Lemma 3.10 Step 5's branching domination, the exact record counts on pp. 38–39 and 42–44, the exact exponents of Lemma 18.2's block protocol, the §14.2 eligibility logic, Proposition 16.3's imported certificates) are the edge of this read — and a referee that finds nothing is weaker evidence than a kernel that accepts a proof, which is why the formal object below carries the label and this section carries the register.

The Lean formalization — again the fact that changes the register. Ninety minutes after OpenAI's repository went public on 6 October, agent lanes started committing to a new repository; 32 hours and 1,922 commits later it was tagged v1.0.0 (8 October). Yao Xu (cadamcat/hypercube-ramsey-lean4 — the same author whose Lean proof of OpenAI's Hindman theorem we are replaying for #172) published a Lean 4 proof of Erdos181.erdos_181: ∃ C > 0, ∀ n, R(Q_n) ≤ C·2ⁿ, with the cube, the Ramsey number and the statement copied verbatim from DeepMind's Formal Conjectures. 752 files, 532,000 lines of Lean, written by AI agent lanes (by file tag mostly GPT-6.1 Sol, with Claude Opus and others) under a human who planned and dispatched; its own metadata says agent-reviewed, reviewers: none, and 39 commits are titled "WIP before escalation (may not compile)" — none of them is the tag. It depends on OpenAI's own Lean library at the release commit (which supplies only the cube graph, the Ramsey number, the elementary bounds 2ⁿ ≤ R(Q_n) ≤ 4²ⁿ and Lemma 2.1 — 287 lines; OpenAI did not formalize Theorem 1.1) and on Mathlib at a pinned commit — the same 43 pinned package revisions as the Hindman project, which is why our replay can reuse that build. We audited the source without building it: the statement and its three definitions are a byte-for-byte copy of Formal Conjectures' file at the pinned commit (the current file changes only the category attribute); C is bound outside ∀n; the sInf ∅ = 0 trap in ℕ's infimum is closed because the bridge to OpenAI's definition is an equality of sets in both directions and OpenAI's library proves the set nonempty; an audit file restates the theorem in plain colouring terms and proves it equivalent; no axiom, live sorry, native_decide or environment-editing code reaches the proof (OpenAI's one axiom and its sorries live in an unimported challenge directory); Mathlib, Batteries and Lean core are pristine checkouts and OpenAI's 23 compatibility patches touch none of them. The author reports a from-source build and #print axioms = propext, Classical.choice, Quot.sound, plus a second-kernel check. On the strength of that, Formal Conjectures marked erdos_181 research solved on 11 October at 07:56Z — via pull request #7128, authored by the formalizer himself, approved 32 minutes after it opened by a DeepMind maintainer ("Thanks, great to have a formal proof!") in a batch of about twenty such PRs that hour, merged at 09:09Z, with no rebuild — FC's CI cannot build a linked external proof. The author's own bounty claim for it (Justin Sun Prize, JSP-000175, open) says so in as many words: "The author ran the check; no independent person has reviewed the formalization … The raw logs are not published … Independent verifier(s), if any: none." Nobody else has reported a build. Ours would be the first.

Our replay. That report is the author's observation, not ours, and this site's CLOSED badge promises an independent check. So the same build is queued on our own machine — scrubbed environment, from the pinned sources, lake build HypercubeRamsey.Main then scripts/verify.sh (statement comparison against the Formal Conjectures file, then #print axioms under --trust=0) and the two audit files — behind the #172 replay whose 22 GB of built dependencies it reuses, at the lowest priority on a box carrying a SAT sweep. As this page went live (11 October, ~13:0xZ) the #172 build ahead of it stood at 10,86x of 10,995 jobs. It finished: 9,650 jobs built from the pinned sources in 5 h 08 min at nice 19 on four threads (the driver was relaunched at 18:02Z after a first attempt died on a missing lake launcher in the scrubbed toolchain copy — a driver bug, not a Lean one), no errors; scripts/verify.sh reported the Challenge and Main statements identical under pp.all, and #print axioms Erdos181.erdos_181 under --trust=0 printed exactly [propext, Classical.choice, Quot.sound] — the three axioms every Mathlib theorem carries and nothing else; no sorryAx, no custom axiom. Both audit files (Audit/TargetProbes.lean, Audit/IndependentRestatement.lean) compiled under --trust=0 on the same build, their probes carrying the same three axioms. So the kernel accepted, on our machine, a proof of the statement erdosproblems.com/181 asks about. This entry is now CLOSED and #181 joins the problems closed in the literature. The replay driver, steps.tsv, the axiom output and the build log are in the bundle. One honest limit, the Lean-audit seat's procedural finding: in Lean 4.34 --trust=0 no longer re-checks imported modules, so what this run kernel-checked from source is the proof itself and OpenAI's library, while Mathlib's object files came from the official cache (lake exe cache get, 196 s); the leanchecker --fresh HypercubeRamsey.Main pass over the whole import closure, Mathlib included, started at 23:26Z on 11 October and exited 0 after 2 h 10 min (7,773 s): a fresh kernel re-checked every imported module, Mathlib's cached object files included, and printed no error — its only output was Lake's "has local changes" warning for each vendored package the OpenAI patch script edits. What silence means was checked with two controls on the same build (replay/leanchecker_controls.log): a module that does not exist exits 1 with Could not find any oleans; a real module exits 0 printing nothing. That closes the last stated limit of this replay; the log is replay/leanchecker_fresh.log.

Labels. The theorem: (d) computer-assisted — a kernel-checked proof exists, written by a third party following the paper, author-reported replays, and our own from-source replay printed the same three standard axioms (the leanchecker --fresh pass over Mathlib's cached object files exited 0 after 7,773 s). The paper as written: (c) plausible/unverified by a human — nine tool-equipped machine seats with disjoint scopes, each briefed to refute, found no mathematical gap, one exposition gap and one step they could not check line by line; what they skimmed is listed above. The citation checks and our own spot reads are (a)/(b), ours. Nothing mathematical here is ours; the theorem is OpenAI's, the formalization Yao Xu's. The teorth database still says OPEN and unformalized; erdosproblems.com/181 shows no status and does not mention OpenAI; Bloom's 8 October post lists the claim as "not formalised" (true when written) under his blanket "I have checked nothing"; we found no human proof, no improvement on Tikhomirov, and no public comment from Tao, Conlon, Fox, Sudakov, Lee or Tikhomirov.