VibeMathedMath problems solved with AI

The combinatorial invariance conjecture for Kazhdan-Lusztig polynomials

For a Coxeter system (W,S)(W,S) with Bruhat order ≤\le and u≤bu\le b, the Kazhdan-Lusztig polynomial Pu,b(q)P_{u,b}(q) is defined algebraically, through the Hecke algebra and the simple generators, while the Bruhat interval [u,b]={x:u≤x≤b}[u,b]=\{x:u\le x\le b\} is a finite graded poset that remembers neither generators nor root labels. The combinatorial invariance conjecture, attributed to Lusztig and to Dyer, asserts that the polynomial depends only on the interval as an abstract poset. Known before this work: principal lower intervals [1,b][1,b] (du Cloux, Brenti, Brenti-Caselli-Marietti, Delanoy), invariance of the coefficient of qq (Patimo; Barkley-Gaetz-Lam), and full invariance in interval rank at most six, or up to ten or twelve in some finite Weyl groups. If [u,b][u,b] in (W,S)(W,S) and [u′,b′][u',b'] in (W′,S′)(W',S') are isomorphic as posets, is Pu,b(q)=Pu′,b′(q)P_{u,b}(q)=P_{u',b'}(q)?

Result
Proved(see note)
Status
Candidate (review pending)
AI contribution
AI-discovered
Method
Argument
Field
Algebraic combinatorics: Kazhdan-Lusztig polynomials and Bruhat order
Posed by
George Lusztig and Matthew Dyer; published formulation in M. Dyer, On the Bruhat graph of a Coxeter system, Compositio Math. 78 (1991), Section 3.5
Year posed
1991
Years open
35y
Solved
2026-09-24
Model
Unreleased internal OpenAI model
Vendor
OpenAI
Collaborators
—
Verification
Lean-checked, statement unaudited
Publication
Announced
Collection
OpenAI math release (October 2026), version adc7f12
Significance
52 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

Theorem 1.1: for arbitrary Coxeter systems (W,S)(W,S) and (W′,S′)(W',S'), including infinite and noncrystallographic ones, and u≤bu\le b, u′≤b′u'\le b', any poset isomorphism [u,b]→[u′,b′][u,b]\to[u',b'] gives Pu,bW=Pu′,b′W′P^W_{u,b}=P^{W'}_{u',b'} for the equal-parameter polynomials; restricting to subintervals determines every Px,yP_{x,y} and, by reciprocity, every RR-polynomial on the interval. The proof uses moment-graph sheaves (Braden-MacPherson, Fiebig, Elias-Williamson), an edge schedule transported from a reflection order of the second system, and Dyer's path formula. It gives no procedure computing PP from the poset, and it treats equal parameters only.

What the AI did

The OpenAI math release (github.com/openai/math, commit adc7f12) states that its results were produced by an unreleased internal OpenAI model under one fixed procedure, averaging about three hours of ChatGPT Pro thinking compute per result, across roughly 4,000 posed problems; outputs were then grouped into families and filtered for significance. This result is not among the README's stated exceptions (the Riemann zeta zero-free region work and the Hodge conjecture for CM abelian varieties). The manuscript is credited to OpenAI alone and names no human author.

Verification

No independent mathematician has checked this yet. Checked here: the abstract, introduction and Theorem 1.1 of the TeX source, read against the conjecture as the manuscript cites it; the proof was not refereed. Lean: the Comparator challenge KLInvariance (OAI.KLInvariance.combinatorial_invariance, solution module OAI/RepresentationTheory/KazhdanLusztig/Invariance.lean) is not in the release's formalization catalogue, but its JSON and solution file exist at the pinned commit. Its statement was read here: for two Coxeter systems on arbitrary groups, an order isomorphism between strong Bruhat intervals (Bruhat order defined as the reflexive-transitive closure of length-increasing reflection steps) gives equal Kazhdan-Lusztig polynomials. The polynomials are the family chosen (by Classical.epsilon) among those satisfying the R-recursion, the degree bound and the reciprocity identity, so the statement is the headline claim provided that normalization singles out the classical polynomials, which is standard but is part of the encoding. Permitted axioms: propext, Quot.sound, Classical.choice. Not rebuilt here.

Sources

Changelog1 change

Discussion