---

Claim. The preprint Monochromatic finite sums and products in the positive integers of the OpenAI mathematics release (dated 23 September 2026, authored by OpenAI) states as its Theorem 1.1 that for all integers $r,m\ge1$ and reals $R\ge2$, $D\ge1$, every coloring $\chi:\mathbb N\to[r]$ admits distinct positive integers $a_1<\cdots<a_m$ and a color $c$ with

$$\chi\Bigl(\sum_{j\in J}a_j\Bigr)=\chi\Bigl(\prod_{j\in J}a_j\Bigr)=c \qquad\text{for every nonempty }J\subseteq[m],$$

and moreover $a_1>R$ and $a_d>R\bigl(\sum_{k<d}a_k+\prod_{k<d}a_k\bigr)^D$ for $2\le d\le m$. Its Corollary 1.2 draws from the separation that the $2^m-1$ subset sums and the $2^m-1$ subset products are each distinct and meet exactly in the $m$ singletons. The theorem is the statement of Problem 172 for every size $m$ and every finite coloring, in the reading the problem page fixes (Hindman's conjecture; Alweiss's Conjecture 1.1): all sums and products of distinct elements of an $m$-element set in one color. The manuscript is carded at openai_2026_monochromatic_finite_sums_products_positive_integers, with its main statements paged there. It names Hindman's finite sums and products conjecture as what it proves, notes that the statement for colorings of $\mathbb N_0$ follows by restriction, and distinguishes it from the false infinite version, Hindman's 1980 coloring recorded on the problem page. Its history section cites the partial results the problem page records (Graham and Hindman's computer-assisted $\{x,y,x+y,xy\}$ for two colors, Bowen, Moreira, Alweiss, Bowen and Sabok, and Alweiss's theorem over $\mathbb Q$) and says that the passage from $\mathbb Q$ to $\mathbb N$ needs more than clearing denominators, since a dilation scales sums and $j$-fold products by different powers. The release's README says its manuscripts were produced by an unreleased internal OpenAI model and come at different stages of verification, not all with Lean formalizations.

Method and read depth. By the introduction, the proof selects ordered blocks of widely separated variables whose block products already have one color by a Ramsey argument and the finite sums theorem, and then arranges that their sums take the same color through two principles: a Prediction Principle, which replaces the color indicators in the relevant counts by piecewise nilsequences while keeping the multiplicative color masks, and an Alignment Principle, which chooses rational scale vectors from a finite list so that positive predictions survive the required additive shifts, with a success probability independent of the model complexity through polynomial recurrence in a nilpotent group. The inputs named are the inverse theorem of Green, Tao and Ziegler, the concatenation theorem of Tao and Ziegler, quantitative polynomial equidistribution and nilpotent polynomial recurrence; the manuscript says all parameters are qualitative and claims no numerical bound for the smallest configuration. This page rests on the abstract, the introduction and the statements of Theorem 1.1 and Corollary 1.2; no proof is checked, and nothing here is review.

Depends on. Nothing in this wiki; the manuscript's own argument carries the claim.

Formalization. None of the theorem. The release's Lean tree at the pinned revision has no comparator challenge and no catalog entry for this manuscript. It holds a development OAI/Combinatorics/SumProduct/Alignment/ of 259 files without sorry, imported by the project's root module through its Main.lean, which only aggregates imports. Its top declaration, SourceRawMenu.alignment in RawMenu.lean (re-exported as raw_alignment_reference), states and proves the manuscript's Principle 2.4 (Alignment): for all parameters there are a finite list of scales, a finite list of positive rationals and a $\delta>0$ such that, for every admissible family and every system of models, the lower limit of the probability of the alignment event is at least $\delta$, independent of the tolerance and of the model complexity. On the way, WordPlan01.lean proves coloring_polynomial_recurrence and coloring_recurrence, polynomial recurrence for colorings of nilpotent groups, with supporting lemmas on rational lattices, Malcev coordinates, polynomial Weyl sums and cube faces. The development does not state Theorem 1.1, the Prediction Principle (2.3) or the deduction of the theorem from the two principles (Section 2.5), so it is a formalization of one ingredient and not of the claim; nothing was built or audited here. The formal-conjectures statement of the problem, on the problem page, is a statement without proof.

Standing. Claimed. The manuscript is a release preprint with no journal record and no independent review known to this corpus; the site's page for Problem 172, shows OPEN with an empty proof-claim tab. A refereed version or a documented independent acceptance would move the claim to accepted; until then the problem's standing is claimed through this page.