The combinatorial invariance conjecture for Kazhdan–Lusztig polynomials
From OpenAI Aftermath
The combinatorial invariance conjecture for Kazhdan–Lusztig polynomials asks whether the polynomial Pu,b(q) attached to a Bruhat interval [u, b] of a Coxeter group depends only on the interval as an abstract partially ordered set. The conjecture is attributed to Lusztig and to Dyer. A manuscript dated 24 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims a proof for arbitrary Coxeter systems, also when the two intervals come from different Coxeter systems. The collection includes a Lean formalization of this statement. This page summarizes the published claim 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 introduction of the manuscript:
- Kazhdan and Lusztig introduced the polynomials through the canonical basis of the Hecke algebra and interpreted them through intersection cohomology of Schubert varieties. Dyer showed that the interval order determines the directed Bruhat graph, but not the root labels.
- For principal lower intervals [1, b], invariance was proved by du Cloux for a class including finite and affine groups, by Brenti for symmetric groups, and by Brenti, Caselli and Marietti and by Delanoy for arbitrary Coxeter systems.
- For general intervals, Incitti treated short intervals in classical types; Patimo and then Barkley, Gaetz and Lam proved invariance of the coefficient of q, the latter deducing full invariance in rank at most six; Esposito, Marietti and Stella reached rank ten in finite Weyl groups and rank twelve in type A. Blundell, Buesing, Davies, Veličković and Williamson proposed a hypercube recurrence guided by machine-learning models, later proved by Barkley and Gaetz for principal lower intervals in symmetric groups.
The original result
- Claim. Theorem 1.1 of Combinatorial invariance of Kazhdan–Lusztig polynomials states that for arbitrary Coxeter systems (W, S) and (W′, S′), every isomorphism of Bruhat interval posets [u, b] → [u′, b′] implies PWu,b(q) = PW′u′,b′(q), including for infinite and noncrystallographic groups; a corollary recovers all polynomials and R-polynomials of the subintervals.
- Method, as described: the proof works in the moment-graph form of the theory, in the tradition of Goresky–Kottwitz–MacPherson, Braden–MacPherson, Soergel, Fiebig and Elias–Williamson, after a closure proof, for arbitrary Coxeter systems, of Dyer's reconstruction of the directed Bruhat graph from the order, followed by localization and comparison arguments.
- Sources. The manuscript Combinatorial invariance of Kazhdan–Lusztig polynomials at commit
1581d4c. - Formalization, as described by the repository. The scope note states that the formalization proves that every order isomorphism between Bruhat intervals in arbitrary Coxeter systems preserves the corresponding equal-parameter Kazhdan–Lusztig polynomial, the two intervals possibly coming from different Coxeter systems. The Comparator statement is
KLInvariance.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 20 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full", stating that the challenge allows different Coxeter groups, uses the genuine strong Bruhat order, and normalizes the polynomials by the standard Kazhdan–Lusztig characterization. It records a sandboxed Comparator pass. | MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-09 | N. Libedinsky, arXiv:2610.14275, Polytopal invariance for Lusztig's q-weight multiplicities | Related (cites) | Proves that isometric polytopes attached to pairs of dominant weights have equal Lusztig q-analogues of weight multiplicities, across Dynkin types, and constructs the polynomial from the metric shape of the polytope. The paper states that a conjecture it formulates, combined with the combinatorial invariance conjecture, whose proof it describes as recently announced by OpenAI, would imply its main theorem. | arXiv preprint. |
| 2026-10-10 | cert-machine, openai/math lane K: run 38040214623 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the KLInvariance solution, in 1,097 s. The project reports two-kernel certification of 398 of 416 challenges of the collection. |
Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) does not list KLInvariance, so it was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-16 | J. Jardine, Lattice24, referee review in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap and no minor notes. The reviewer states that it read all of the LaTeX source and checked the main steps by hand. | Part of an audit of the collection's manuscripts that the audit describes as complete. The review is published under CC BY 4.0. |
Notes
- The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
