#172: OpenAI's proof of Hindman's sums-and-products conjecture — read in full, sources checked, and a third-party Lean 4 kernel check replayed on our own machine

The problem (erdosproblems.com/172; community database status OPEN as of our 11 October refresh). Is it true that in any finite colouring of ℕ there exist arbitrarily large finite A such that all sums and products of distinct elements in A are the same colour? This is Hindman's 1979 question. Hindman himself showed the infinite version fails (a seven-colouring with no infinite such A). Moreira (2017) got {x, x+y, xy} in one colour; Bowen (2022) got {x, y, x+y, xy} for two colours; Bowen–Sabok got the quartet over ℚ; Alweiss (2023, Duke, to appear) got the full statement — every nonempty subset sum and product — over ℚ. Our own August working report reduced the ℕ question to finite weak-hypergraph thresholds R(r,k) and computed the smallest of them (R(2,2)=8, R(3,2)=100, R(2,3)>5000, pairwise reading); it did not touch the infinite question.

What OpenAI claims. Monochromatic finite sums and products in the positive integers (23 September 2026, family 164 of the 6 October release, 70 pages, no Lean in the release). Theorem 1.1: for every r-colouring of ℕ and every m there are a₁ < ⋯ < a_m with every nonempty subset sum and every nonempty subset product in one colour — and the a's can be chosen so separated (each exceeds a prescribed power of the sum-plus-product of its predecessors) that all 2(2^m−1)−m expressions are distinct. That is the ℕ statement under every reading of "sums and products of distinct elements": pairwise sums and products are the 2-subset ones. A compactness corollary (2.6) gives finite thresholds — our R(r,k) are finite — with, the paper says plainly, no numerical bound.

How the proof is built (plain version). The multiplicative half is cheap: a Ramsey-plus-finite-sums selection, lifted from Alweiss's rational argument, picks "block products" of widely separated variables whose nonempty products already share a colour. The whole paper is about making their sums land in that colour too. Two principles do it. Prediction (§3–5) replaces the colour-indicator functions inside a weighted count by bounded "piecewise nilsequence" models — Green–Tao-style transference with divisor weights, Cauchy–Schwarz mask removal, a dense-model theorem, and the Green–Tao–Ziegler inverse theorem — while keeping the product masks exact. Alignment (§6–8) chooses, from a fixed finite menu of rational rescalings, one under which every positive prediction survives all the required additive shifts; it is a van der Waerden-type recurrence in a nilpotent group of transformations (Zorin-Kranich's nilpotent IP polynomial recurrence), fed by a progression-comparison theorem that strips a "rough" step out of a nilsequence sample and a lifting theorem that makes symmetries of one marginal act on a joint state. The success probability of Alignment is bounded below independently of the models' complexity — that uniformity is the hinge, and the paper is explicit that the order of choices (Alignment's δ before Prediction's complexity) is what makes the calibration error small enough.

What we checked ourselves. (1) The §2 deduction of the theorem from the two principles, line by line: the chain condition that makes each earlier block an "adding pair" of each later one, the integrality of every colour argument, the quantifier order τ → η → N → w along the ultrafilter, and that positivity of the weighted count yields an actual configuration (the divisor weights only restrict which tuples count). (2) Every external theorem the paper leans on, against the current arXiv version: Zorin-Kranich's Corollary 3.7 (v4) says what §8.1 uses, including the handedness the paper flips by inverting words; Tao–Ziegler's Theorem 1.23 (v4) is exactly inequality (5.11) with the modulus depending only on rank and order; the Green–Tao–Ziegler erratum (2024) corrects Proposition 8.3 and filtration tautness and leaves the inverse conclusion the paper uses; the Green–Tao erratum (v3) proves the multiparameter equidistribution theorem precisely in the equal-sides case Theorem 6.1 uses; Alweiss's Theorem 1.3 and Proposition 4.1 (v6) are the ℚ theorem and the rescaling mechanism (8.1)–(8.2) adapts. Verbatim quotes are in the bundle. (3) Two exact controls with a negative control each: identity (8.2) — the rescaling exponent λ_e is positive for every pair at a pivot — exhaustively for n ≤ 8 (37,133 cases, 0 violations); and Corollary 1.2's separation argument (3,000 random separated sets, all injective with FS ∩ FP = A; 3,000 unseparated sets, 1,271 collisions, so the checker can fail).

The paper as written — a four-seat hostile read. Separately from the formal proof above, we refereed OpenAI's 70-page preprint the way we referee our own work: four tool-equipped Opus seats with disjoint scopes (§2 the deduction; §3–5 the Prediction Principle; §6–8 the Alignment Principle; the bibliography and the live world), each briefed to refute, to fetch every cited theorem from its current arXiv version rather than from memory, to quote the sentence it objects to, and to say which steps it verified line by line and which it only skimmed. One of us read §2, §4.1, §5.3, §6.1 and §8 independently before the seats reported. Every objection below carries its quote in the bundle.

§2, the deduction (seat: deduction) — HOLDS AS READ. Theorem 1.1 and Corollaries 1.2 and 2.6 follow from the two principles exactly as the principles are worded; the parameter graph m → s(m) → n(m,r) → (𝓑, 𝓐, δ) → τ, η → models has no cycle; the chain selection (Lemma 2.5) is Sanders's Lemma 1 plus the finite-sums theorem, with the tails co-ordered with the pivots — a necessary change from Alweiss's Step IV (his anti-ordered tails fail the adding-pair condition (2.1) on every pair, by our control), and the paper discloses the change. Every inequality in §2.5 re-derived, including the τ^2m−m−1 ≥ τ^2m step and the Kη margin; positivity of the weighted count does force an actual monochromatic set because every factor is nonnegative and every sum point is a positive integer for large w; the separation (1.1) follows from Definition 2.1's domination clauses. Four cosmetic notes (an ultrafilter limit applied to a count not shown bounded — harmless, the terms are nonnegative; finitely many small w where the colour arguments are not yet integers; an uncited lemma of Sanders; reused symbols). What §2 cannot settle it names: that s depends on m alone, that δ is uniform over nilmanifolds of every dimension and every Lipschitz constant, and that alignment defeats model pieces that are arbitrary functions of the residue mod M. Those live in the two principles.

§3–5, the Prediction Principle (seat: prediction) — HOLDS AS READ. The seat set out to break Principle 2.3 and could not. It traced every constant to its inputs: the number of mask-removal rows (≤ (2^m−1)·2^2m−1), the cube dimension d, the subgroup-norm order 2^d, the global Gowers order 2^d+1−1 and hence the nilpotence step 2^d+1−2 ≤ s all depend on m alone, which is what §2 needed; the dense-model tolerances ζ, J₀, ε are fixed before the master count N; the models are chosen after the Ramsey selection and may depend on everything, as Principle 2.3 allows. No cycle. The four external inputs were fetched and compared sentence by sentence: the Green–Tao–Ziegler inverse theorem in its linear-nilsequence form (Conjecture 1.2 + Theorem 1.3; the current arXiv v5 of 23 April 2026 restates both word for word; the 2024 erratum withdraws Proposition 8.3 and says the Appendix C lifting survives under the tautness condition G₀ = G₁, and the paper uses only the inverse conclusion, as it says) — MATCH, including the complexity notion (finite list of nilmanifolds, sup and Lipschitz bounds, no bound on g or x) that Definition 2.2 relies on; Tao–Ziegler's Theorem 1.23 (qualitative Bessel inequality, constant depending only on rank and degree, "independent of the size of I"), applied with rank-zero coset progressions = finite subgroups — MATCH; Yamada's Theorem 2 (explicit Brun–Titchmarsh) — MATCH; the Gowers / Reingold–Trevisan–Tulsiani–Vadhan dense-model attribution — a method citation only, since the paper re-proves its Proposition 5.2 from its own Lemma 5.1, so no pseudorandom-majorant hypothesis is imported unverified: the linear-forms condition the divisor weights need is Proposition 3.6, proved in the paper, and the seat re-derived its local-factor bounds. Verified line by line: Lemma 3.1 (all three sampling identities), Corollary 3.2, Lemma 3.3 against Definition 2.1 (the super-increasing exponents h_j = W^w2N−j give integral ratios on exactly the adding pairs), Lemma 3.5, Proposition 3.6, Lemmas 4.1–4.4 (the prime-insertion trick — harmonic measure is nearly dilation-invariant, so z ↦ pz costs o(1) and a weighted Cauchy–Schwarz removes each product mask, the Green–Sanders mechanism carried to ℤ by the divisor weights), Proposition 4.5, Lemmas 5.1–5.5, §5.4's two telescopes, and the missing-corner Lemma 7.2. Objections, all cosmetic: the erratum's month; two mis-described Cauchy–Schwarz directions in the proof of (5.13) ("translating the root alone" — the direction moves every vertex; what matters is that it fixes the density factor, and the count 2^d of eliminations is right); a CRT hypothesis in Proposition 3.6 that controls residues mod p while the local factor depends on residues mod p^A — correct as the proof actually uses it (it only ever swaps the uniform law inside a β-bound), but the wording invites the wrong reading. Skimmed, not re-derived: the countable diagonalisation of Remark 3.4, PNT in progressions at a fixed modulus, the rationality of lower-central terms, and exact numerical constants. Told afterwards that the third-party formalisation had swapped exactly these two inputs, the seat re-read both §5.3 applications clause by clause: dropping Tao–Ziegler's dilates is exact for finite subgroups and their multiset sum is the uniform measure on the subgroup sum, so (5.11) is the theorem's own statement; on one cyclic cell the cyclic-to-interval estimate (5.14) checks, choosing one period and shifting only the base point is exactly right, and the degree bookkeeping 2(2^d)−2 ≤ s is (5.1) — indeed d ≥ 2 always, so only GTZ's Theorem 1.3 is ever invoked. The Lean project's substitutions reflect what was available to formalise, not a misquotation in the paper.

§6–8, the Alignment Principle (seat: alignment) — HOLDS AS READ. This is where the paper's strongest uniformity lives — finite lists and a δ > 0 depending only on (n, r, s) that work against models of any complexity — and where a machine-written proof would most plausibly assert what it had not proved. The seat traced δ to its definition (8.26), δ = ∏ 1/(3Q_iV_i), with the option and slot counts coming from Lemma 8.1's finite word plan, "before the choice of admissible parameters, models, and τ", and checked the three links that make it complexity-free: (1) nilpotent polynomial recurrence is used only as a colouring statement — Zorin-Kranich's Corollary 3.7 (current arXiv v4 of 4 June 2018, as cited; quoted and compared, including the paper's handedness inversion, and the IP-polynomial claim, which is the source's own Corollary 2.26 under the stretched filtration) — made uniform over every class-≤s action by pulling colourings back from the free nilpotent group on the abstract letters, so no uniform measure bound is imported from anywhere; (2) the lift group has class ≤ s independent of dimension and coefficients (Lemma 7.7, verified: weighted polynomial shears, (T*−1)V_d ⊆ V_d−1, I^s+1 = 0); (3) pointwise coverage becomes mass by closed-set Portmanteau and pigeonhole on the limit Haar measure, (8.23), exact on the limit, with rate-dependent equidistribution entering only the o(1) transfer to the actual sampling — which is all (2.13) asks. The Green–Tao equidistribution input was compared with the 2015 erratum (arXiv:1311.6170v3, as cited): the correction changed the hypothesis (equal sides, or an extra small-side alternative), not the exponents, and the paper uses only equal-side cubes and says so. Verified line by line: (8.1)–(8.2), Lemma 8.1's backward recursion and the compactness/pullback paragraph, the residue bookkeeping (8.9)–(8.11), (8.14)–(8.17), (8.21) — the random rational offset is realised as an exact integer shift m_eq_e = (h_Ab′_Ad_A/h_Bb′_Bd_B)t_A, exactly the offset in (2.12) — Lemma 8.3 (palette, closedness, coverage, the 3τ/2 : 7τ/4 : 5τ/4 open enlargement), (8.25) against Lemma 3.1, (8.27)–(8.28) and the path iteration, Lemmas 7.1, 7.2, 7.7, Proposition 7.5, Lemma 6.2's exact division after interpolation, and Theorem 6.1 against its sources. Checked step by step but not constant by constant: the Proposition 6.3 induction, Lemma 7.3's descent, Proposition 7.4's remaining parts, Lemma 8.2's exposure. Seven cosmetic notes (a redundant compactness re-derivation; ⊂ for ⊆ in §8's quantifier over D; the source's [N] vs the paper's {0,…,N−1}; "rational element" defined by rational logarithm where Green–Tao define it by a power in Γ — the same thing on a rational Mal'cev structure; a sketched discreteness argument in Lemma 7.3). No step uses a bound on g or x; bounded complexity is used exactly where Definition 2.2 grants it, in Lemma 8.3's compactness of observables.

The bibliography and the live world (seat: citations) — ACCURATE except one attribution. All 37 references exist; all eleven arXiv version numbers and dates match the arXiv record to the day (including the three 2026 revisions the paper leans on: Alweiss v6 of 12 July 2026, "accepted in Duke"; Green–Tao–Ziegler v5 of 23 April 2026, which fixes the filtration in Lemma 13.2; Richter v2 of 7 February 2026); every DOI'd venue, volume and page range matches Crossref or zbMATH. Every theorem-number claim in §1.1 was read in its source and says what the paper says it says — Alweiss's Theorem 1.3 is the full finite theorem over ℚ (for a nonzero n-tuple; distinctness is not in the statement), Bowen's Theorem 1.1, Moreira's Theorem 1.4 / Corollary 1.5, Alweiss–Bowen–Sabok's Theorem 1.2, Green–Sanders's Theorem 1.2, Bowen–Sabok's Theorem 1.1, Richter's Theorems 1.5 and 1.7, and Hindman–Phulara p. 82 on Graham's computer check of [252] (where x = 1 is allowed, so the "quartet" is the triple {1, y, y+1}; Hindman's 990 gives genuine quartets). Three cosmetic defects: the seven-colour counterexample for infinite sets with pairwise sums and products is credited to Hindman's 1980 "Two counterexamples" paper [21], whereas Hindman's own later papers (Hindman–Phulara 2013; Hindman–Ivan–Leader 2022) and zbMATH's review place that construction in his 1984 paper Partitions and pairwise sums and products, JCTA 37, 46–60 ("a seven cell partition of ℕ is constructed with the property that no infinite set has all of its pairwise sums and products in any one cell") — erdosproblems.com/172 cites the 1980 paper for it too, as did our own August report, so the slip is inherited; we have not yet read the 1980 PDF ourselves (ScienceDirect blocks our machines) and say so rather than call the 1980 paper's content; the GTZ erratum [18] is dated "April 2024" and the file is from 25 February 2024; and Discrete Analysis never registered the DOI it prints on Alweiss's 2024 paper [2]. No fabricated bibliographic detail anywhere — the failure mode the brief was written for did not occur.

Novelty. No earlier or independent proof of the finite conjecture over ℕ exists on arXiv (nine targeted searches, 2023–2026). The literature calls even the two-element case open for general colourings: Green–Sawhney (Nov 2025), Alweiss–Bowen–Sabok (Dec 2025, "recalcitrant for decades"), Richter (Feb 2026, "remains open"); the FrontierMath Erdős paper (Adamczewski–Bloom, 6 Sept 2026) lists #172 among 68 problems open as of August 2026; Richter–Tsinas, posted 24 September and revised 8 October 2026, still call {x, y, x+y, xy} "a central open problem". The preprint is not on arXiv; OpenAI's repository has issues disabled, so no public correction can be filed there; family 164 was untouched by the 7 October withdrawals. Bloom's 8 October post lists #172 as a claim, 70 pages, not formalised, with his blanket "I have not yet looked in any serious way at any of the proofs". The teorth database and Formal Conjectures still say OPEN — a blanket non-update that also covers the Lean-formalised claims, not a verdict on #172. No public comment from Tao, Alweiss, Bowen, Moreira or Richter found; nothing on MathOverflow.

Verdict on the paper as written: HOLDS AS READ, four seats out of four, no objection above cosmetic. Each seat was briefed that the base rate for a machine-written 70-page higher-order-Fourier proof of a famous conjecture is low and that its job was to find the sentence where it fails; none found one, and the one place every seat pointed at in advance — the complexity-free δ of Alignment — turned out to be proved by a route (free-nilpotent-group pullback, then pigeonhole on the limit Haar measure) that imports no uniform measure bound from anywhere. What this is not: a human expert's reading, or a check of every constant — the seats list what they skimmed (the Proposition 6.3 induction's weight estimates, the Remark 3.4 diagonalisation, Lemma 7.3's descent, PNT in progressions at a fixed modulus, the rationality of lower-central terms) — and a referee that finds nothing is weaker evidence than a kernel that accepts a proof, which is why the formal object above carries the label and this section carries the register. Our own whole-paper seat (one Opus referee with tools, all eight sections plus the five cited sources at their current arXiv versions, briefed to refute) landed after this page went live and also reads HOLDS AS READ: it pressed the §2.5 deduction, all five external citations and eight named pressure points, and "every objection dissolved on inspection". It found two expository defects and one attribution note. The Cauchy–Schwarz procedure the paper describes for inequality (5.13) in Lemma 5.5 is not the one that yields it — the directions it inserts fix more vertices than stated and the shift density is not invariant under them — but a single Cauchy–Schwarz step in the root-only direction gives the same inequality with the same exponent, so the step is true as stated and only its exposition is wrong; the paper writes ⊂ for ⊆ throughout, which matters only if a reader takes (8.18)'s "D ⊂ E_B" as proper; and Lemma 2.5's block ordering is not Alweiss's (the paper says so, and its proof stands alone). It lists what it checked only in outline: the term-by-term pairwise independence of every form in the expanded Cauchy–Schwarz systems of Lemmas 4.4 and 5.1, the explicit constants of §3, and Proposition 7.4's uniformity over boxes. Its own small numerical controls are in the bundle too — among them Lemma 6.2's exact-division claim, which holds in 60 of 60 random instances under the paper's domination hypothesis and in 0 of 60 without it, so the checker can fail. Its report sits in the bundle beside the four sectioned ones.

The Lean formalization — the fact that changes the register. On 7 October Yao Xu (cadamcat/hindman-sums-products-lean4) published a Lean 4 proof of hindman_finite_sums_products: for every r, χ : ℕ → Fin r and m there is an m-element set of positive integers with every nonempty subset sum and product coloured c — Theorem 1.1 without its separation clause, and (a file added 11 October) exactly the statement in DeepMind's Formal Conjectures for Erdős #172 derived from it. 84 files, 6.0 MB of Lean; written with Claude Opus 5.5 and GPT-6 models under a human who "planned, dispatched and reviewed". We audited the source: the only sorry is the Comparator challenge placeholder, no axioms are declared, no native_decide. The structure is the honest part: the Alignment Principle is not re-proved there — it is imported unchanged from OpenAI's own library, where charted_finite_menu_alignment sits in 259 sorry-free files that the release index never mentions (OpenAI formalized the hardest half and stopped short of the theorem; the release lists family 164 as having no Lean). The Prediction half is the third party's own, with two substitutions: Tao–Ziegler concatenation replaced by Kravitz–Kuca–Leng's subgroup box-norm concatenation, and the Green–Tao–Ziegler inverse theorem replaced by OpenAI's cyclic inverse theorem (formalized for the reciprocal-sum family). So the formal object certifies the theorem, by a route that departs from the paper's §5 text at exactly the two places where the paper cites the heaviest outside machinery. The author reports a from-source build (11,472 jobs), #print axioms = propext, Classical.choice, Quot.sound, a 30-minute leanchecker --fresh kernel replay, and a second replay in nanoda, an independent checker, with sorry and altered-numeral controls rejected.

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 running on our own machine — scrubbed environment, from the pinned sources, lake build then #print axioms under --trust=0 — on a box already carrying a SAT sweep, at the lowest priority. As this page went live (11 October, 07:1xZ) the build stood at 8,961 of 9,244 jobs. It finished: 11471 jobs built from the pinned sources in 8 h 21 min at nice 19 on four threads, no errors, and #print axioms hindman_finite_sums_products 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. The non-vacuity audit (parity colouring, m = 3, the empty-subset guard) ran clean on the same build. So the kernel accepted, on our machine, a proof of the statement erdosproblems.com/172 asks about. This entry is now CLOSED and #172 joins the problems closed in the literature. The replay log and the axiom output are in the bundle. One honest limit, found by the Lean-audit seat of our #181 read: in Lean 4.34 --trust=0 no longer re-checks imported modules, so what this run kernel-checked is everything it compiled from source — the proof itself and OpenAI's library — while Mathlib's object files came from the official cache unchecked; the leanchecker --fresh pass over the whole import closure, Mathlib included, ran after our #181 replay (relaunched at 03:05Z on 12 October after the driver's first attempt died on a missing lake launcher in the scrubbed toolchain copy — a driver bug, not a Lean one) and exited 0 after 13,271 s (3 h 41 min), printing only Lake's "has local changes" warnings and no error line; the negative control for reading that silence as a pass ran on the same build (a non-existent module exits 1 with "Could not find any oleans"); the positive control on this build was stopped by us at 28 GB of memory to protect a loaded box, and the identical binary's positive control on our #181 and #1083 builds exited 0 printing nothing. So Mathlib's cached object files are now kernel-checked too, and nothing in the import closure was rejected.

Labels. The theorem: (d) computer-assisted — a kernel-checked proof exists, written by a third party following the paper, author-reported kernel and nanoda replays, and our own from-source replay printed the same three standard axioms. The paper as written: (c) plausible/unverified by a human — four tool-equipped machine seats with disjoint scopes, each briefed to refute, each reporting HOLDS AS READ with only cosmetic objections; the seats' skim lists are in the bundle. The §2 deduction, the citation checks and the two controls above are ours, (a)/(b). Nothing mathematical here is ours; the theorem is OpenAI's, the formalization Yao Xu's. The teorth database still says OPEN; Open Proof Network still says open (its only recorded attempt, "AlphaProof Nexus, Feb 2026", not solved); Bloom's 8 October post lists #172 among the 25 Erdős claims and endorses none; we found no human-written proof on arXiv.

What our August numbers now mean. R(2,3) > 5000 was the smallest unsettled finite case under the pairwise reading; the theorem says every R(r,k) is finite and gives no estimate, so that colouring is just a lower bound on a number now known to exist. The gap between "exists" and "is less than 10^?" is where the finite question lives now.