The Eisenbud–Green–Harris and lex-plus-powers conjectures

The Eisenbud–Green–Harris and lex-plus-powers conjectures concern homogeneous ideals in a polynomial ring that contain a regular sequence of forms of degrees a₁ ≤ … ≤ a_c. The Eisenbud–Green–Harris conjecture predicts that such an ideal has the Hilbert function of a monomial ideal containing the pure powers x₁^a₁, …, x_c^a_c; the lex-plus-powers conjecture strengthens this to graded Betti numbers, with the lex-plus-powers ideal as the extremal ideal. Two manuscripts dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claim both conjectures over every field of characteristic zero, for regular sequences of any length with degrees at least two. The collection includes no Lean formalization of these results. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

Background

As recounted in the introductions of the manuscripts:
- Eisenbud, Green and Harris formulated the conjecture in their work on higher Castelnuovo theory. The lex-plus-powers conjecture is generally attributed to Charalambous and Evans; without a prescribed regular sequence, the extremality of lex ideals is the theorem of Bigatti, Hulett and Pardue, and for ideals already containing the pure powers the Hilbert-function comparison is the Clements–Lindström theorem.
- For nonmonomial regular sequences, Abedelfatah proved the Hilbert-function statement for full regular sequences of products of linear forms, Caviglia and Maclagan for fast-growing degrees, and Caviglia and De Stefani under the weaker growth condition a_i ≥ Σ_j<i (a_j − 1) for i ≥ 3. Caviglia and Sammartano proved the Betti statement in characteristic zero under a similar growth condition.
- For the Betti comparison with prescribed powers, Mermin, Peeva and Stillman treated ideals containing the squares of the variables, Murai strongly stable ideals plus powers, and Mermin and Murai ideals containing a monomial regular sequence; Mermin and Murai also isolated the reduction to a monomial ideal with the same Hilbert function and no smaller Betti numbers.

The original results

Claims.
- Theorem 1.1 of Commuting Division-Coefficient Forms and the Artinian Eisenbud–Green–Harris Conjecture constructs, for a homogeneous regular sequence f₁, …, f_n in C[x₁, …, x_n] with degrees at least two, commuting linear forms with coefficients in a finite-dimensional central division algebra over a finitely generated extension of C, satisfying triangular power identities adapted to the f_i, whose ordered monomials form a basis of the full polynomial algebra. Corollary 1.2 deduces the Artinian Eisenbud–Green–Harris conjecture over C, and Corollary 1.3 the conjecture over every field of characteristic zero for regular sequences of any positive length, with a lex-plus-powers ideal realizing the Hilbert function.
- Theorem 1.1 of The Artinian Lex-Plus-Powers Betti Theorem states that, for every ideal of C[x₁, …, x_n] containing a regular sequence of degrees 2 ≤ a₁ ≤ … ≤ a_n, the corresponding lex-plus-powers ideal has the same Hilbert function and every graded Betti number at least as large. Corollary 1.2 extends this to every field of characteristic zero and to regular sequences of any positive length, using the Artinian reductions of Caviglia–Maclagan and Caviglia–Kummini and a descent through the coefficient field.
Method, as described: the division-coefficient forms give an ordered basis in which leading coefficient spaces of an ideal are left ideals of a division algebra, hence zero or everything; their positions define a monomial ideal containing the powers with the same Hilbert function. The Betti manuscript transfers a minimal resolution through this basis to obtain no smaller Betti numbers, then completes the monomial comparison by distractions, a transfer-closed ideal and a Koszul-rank comparison on the extreme slices; it states that this last monomial comparison is not new.
Sources. The manuscripts Commuting Division-Coefficient Forms and the Artinian Eisenbud–Green–Harris Conjecture and The Artinian Lex-Plus-Powers Betti Theorem at commit 1581d4c.
Formalization. The repository has no Lean scope note for this family.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 20 October 2026)
2026-10-07	JuanCaGC/LPPCheck.jl (GitHub)	Support (computational)	An exact computational stress test over Q in Oscar.jl of the three conclusions: that the lex-plus-powers spaces form an ideal, that the Hilbert functions agree, and that the graded Betti numbers are no smaller. The README reports no violation among the instances that completed, with three to five variables, including many degree sequences outside the Caviglia–De Stefani growth condition and instances with fewer forms than variables, and none in an exploration over fields of characteristic 2, 3, 5 and 32003, where the manuscripts claim nothing. It notes that two of Oscar's resolution algorithms returned wrong Betti tables on some ideals and that the minimal-resolution algorithm used was checked against Macaulay2.	The README states that computational evidence is not a proof, that the degree bound used when there are fewer forms than variables is a heuristic, and that the project is not affiliated with OpenAI.
2026-10-16	J. Jardine, Lattice24, referee review of the Eisenbud–Green–Harris manuscript and of the lex-plus-powers manuscript in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995)	Review (AI-assisted audit)	Reports no gap in either manuscript, each with one minor note. For the Eisenbud–Green–Harris manuscript, the cancellation of a scalar cocycle in the determinant-descent lemma of Section 6, which the reviewer calls the crux of the division property, is argued only tersely through weights; the reviewer believes it holds. For the lex-plus-powers manuscript, the proof of Corollary 1.2 cites the Artinian reductions of Caviglia–Maclagan and Caviglia–Kummini without restating their hypotheses; the reviewer believes Theorem 1.1 applies in either form. Both reviews state that every section was read.	Part of an audit of the collection's manuscripts without Lean that the audit describes as complete. The reviews are published under CC BY 4.0.

Notes

The earlier results are due to the authors named in the Background section, as recounted by the manuscripts.
The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.