VibeMathedMath problems solved with AI
Sign in

Polynomial-size black-box identity testing for noncommutative rational formulas

A noncommutative rational formula is a formula with ++, ×\times and inverse gates over noncommuting variables, evaluated on tuples of square matrices where every inverse is defined. Hrubes and Wigderson reduced its identity testing to noncommutative singularity, solved deterministically in the white-box model by operator scaling. In the black-box model, Forbes-Shpilka gave quasipolynomial matrix hitting sets for division-free formulas, and Arvind, Chatterjee and Mukhopadhyay gave deterministic quasipolynomial-size rational matrix hitting sets for rational formulas of any inversion height, asking in their conclusion for polynomial matrix dimension. Is there a deterministic polynomial-time construction of a polynomial-size list of matrix tuples hitting every nonzero rational formula of size ss in nn variables?

Result
Proved(see note)
Status
Candidate (review pending)
AI contribution
AI-discovered
Method
Construction
Field
Algebraic complexity; derandomization of polynomial identity testing
Posed by
V. Arvind, Abhranil Chatterjee and Partha Mukhopadhyay, Black-box identity testing of noncommutative rational formulas in deterministic quasipolynomial time, arXiv:2309.15647 (2023), conclusion
Year posed
2023
Years open
3y
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
32 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

Claims deterministic polynomial-time construction of polynomial-size rational matrix hitting lists for noncommutative rational formulas over Q\mathbb Q, with no bound on inverse nesting or constant heights, each nonzero formula receiving an invertible value. Companions: one rational tuple of dimension at most 2ns22ns^2 hits every nonzero division-free formula over every characteristic-zero field, and an analogous tuple over Fp\mathbb F_p works in each positive characteristic. It does NOT cover general noncommutative circuits, and the rational result is over Q\mathbb Q only.

What the AI did

The release README says all results were produced by an unreleased internal OpenAI model, the vast majority by one fixed procedure using on average about three hours of ChatGPT Pro thinking compute per result. Its named exceptions (the Hodge conjecture for CM abelian varieties, and the Re(s) > 11/12 zero-free region, whose write-up was human edited for readability) do not concern this family. The manuscripts are credited to OpenAI with no human author named. The family has three manuscripts: the rational-formula hitting lists (principal), a single rational hitting point for division-free formulas over every characteristic-zero field (same date), and a positive-characteristic version (4 October). The release formalizes the principal theorem and the single-point theorem in Lean.

Verification

No independent mathematician has checked this yet. Theorem 1.1 of the principal manuscript was read against the question: one deterministic machine, given 1n,1s1^n,1^s, outputs in polynomial bit time a polynomial-size list of rational matrix tuples of a common dimension, one of which gives every admissible nonzero rational formula of size at most ss a defined invertible value. ComparatorChallenges/RationalHitting.lean (OAI.RationalHitting.main, OAI/Computability/RationalHitting/Main.lean, in formalization.yaml) states exactly this, with a TM0 Turing machine, explicit binary output encoding, polynomial bounds on dimension, output length and steps, and inverse gates requiring two-sided inverses. Permitted axioms propext, Quot.sound, Classical.choice. The companion's FormulaHitting challenge (OAI.NCHitting.universal_hitting, not in formalization.yaml) was also read; it states the single-tuple hitting property but not the construction-time bound. Not rebuilt here.

Sources

Changelog1 change

Discussion