AI Proved What?

Episode 116, October 2026

One point for all?

A claimed single matrix substitution, for each characteristic, that detects every small noncommutative formula, and polynomial hitting lists for rational formulas

Covers result 116 in OpenAI’s catalog: all 3 papers. See its connections to other results and the work it cites.

Play Episode 116: One point for all? A strictly lower-triangular integration matrix, shaded by entry size.

6:42. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00Testing without looking
  2. 1:41The claims
  3. 3:14How the proofs go
  4. 5:43Where it stands

The claims, in plain words

Polynomial identity testing asks whether an expression computes the zero polynomial. With commuting variables, substituting random numbers usually settles it. With noncommuting variables, numbers are not enough: x1x2 − x2x1 is zero at every pair of numbers, yet it is a nonzero noncommutative polynomial. So one substitutes matrices. A formula is a tree of additions and ordered multiplications with variables or constants at the leaves, and its size counts every vertex. A small formula can hide many words: the product of k copies of x1 + x2 has 4k − 1 vertices and 2k words. And a fixed small dimension cannot work: by the Amitsur–Levitzki theorem, the 24-term standard polynomial in four variables vanishes on all 2-by-2 matrices.

When the formula can be read, Raz and Shpilka gave a deterministic polynomial-time test, building on Nisan’s rank characterization. In the black-box setting one may only evaluate: Bogdanov and Wee gave a randomized matrix test, Forbes and Shpilka deterministic hitting sets of quasipolynomial size over large enough fields, and Arvind, Chatterjee and Mukhopadhyay quasipolynomial hitting sets for formulas with inverses.

Result 116 is three OpenAI preprints. The first (13 pages, September 24, 2026) constructs in deterministic polynomial time one tuple of rational matrices of dimension at most 2ns² such that every nonzero formula of size at most s in n variables, over any field of characteristic zero, is nonzero there: a single matrix evaluation decides whether a formula promised to be that small is zero. Its entries are explicit: (Ti)r,q = (−1)r−q−1/(r·ir−q) for q < r, and 0 otherwise. The second (14 pages, October 4, 2026) does the same for each positive characteristic p, including 2, with matrices over 𝔽p of dimension O(n³s⁶). The third (25 pages, September 24, 2026) treats rational formulas over ℚ, which may also take inverses: a polynomial-size list of rational matrix tuples such that every nonzero formula with a defined matrix evaluation has a defined, invertible value at one of them, with no bound on how deeply inverses are nested. For example, (x1x2 − x2x1)−1 is undefined at every pair of numbers but defined at a pair of 2-by-2 matrices.

What it doesn’t claim

There is no single tuple for all characteristics: the rational tuple serves characteristic zero, and a separate tuple over 𝔽p serves each prime p. The guarantee is for formulas, which have no shared subexpressions (and for acyclic algebraic branching programs); no bound is claimed for general circuits. The bit-time bounds concern constructing the matrices, not evaluating an unknown formula at them.

Where it stands

Posted as preprints
OpenAI, 13, 14 and 25 pages, dated September 24 and October 4, 2026
Peer reviewed
Not yet
Checked in Lean
OpenAI published Lean proofs for the rational tuple and the rational-formula lists, not the positive-characteristic paper; we have not run the checks

Last checked October 19, 2026. The preprints have not been revised. OpenAI published a Lean formalization of the hitting property of the explicit rational tuple (comparator statement), whose dimension 2ns² is part of its definition, in 36 files and 5,803 lines; its construction cost is bounded only in the repository’s own cost model, outside the checked statement. The hitting lists for rational formulas, with their time, output-length and dimension bounds, are formalized against their comparator in 53 files and 15,304 lines. Both counts exclude Mathlib. The positive-characteristic paper is not formalized. We have not run the checks. None of the papers is among those OSVerify reviewed, and we have seen no expert review.

How the proofs go

  1. Words as iterated integrals. Each word becomes a series in one variable: the empty word gives 1, and putting letter i in front integrates the series divided by z + i. These series are linearly independent, so a nonzero polynomial gives a nonzero series. The matrices are these integration operators acting on the first d Taylor coefficients.
  2. How many coefficients? A formula of size s has a path representation with at most 2s states, so its series is a component of a linear differential system with poles at −1, …, −n. Moura’s multiplicity estimate bounds how deeply a nonzero component can vanish at zero, whatever the coefficients: below 2ns². So the first d = 2ns² coefficients show it.
  3. Positive characteristic. Integration divides by whole numbers, differentiation kills pth powers, and the poles can collide. The second paper replaces the derivative by a multiplicative shift z ↦ tz, which divides by tr − 1. A pole argument gives independence, a shifted Wronskian whose leading term is a Vandermonde determinant bounds the order of vanishing, and truncating powers of t yields matrices over 𝔽p.
  4. Inverses. A formula of size s yields at most s + 1 affine matrix pencils of order at most 2s + 1, whose simultaneous invertibility certifies every inverse gate and an invertible output. The list makes every such family of feasible pencils invertible at one tuple, using a rank-expansion bound proved with a Wronskian, lifts into a division algebra, and a fixed integer grid of parameters.

The numbers in the video

  • The 24-term standard polynomial vanished on 200 random 2-by-2 integer tuples but not on a random 3-by-3 one.
  • The series of all 63 words of length at most 5 in 2 letters were linearly independent.
  • 339 different random nonzero formulas of size up to 9 in 2 variables were all detected at the 324-dimensional tuple, none needing more than 6 coefficients; this is a sanity check, not a test of the bound.
  • For X = (0 1; 0 0) and Y = (0 0; 1 0), XY − YX = diag(1, −1) has determinant −1, so its inverse is defined.

Read the source

The 3 papers in this result

OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.

Transcript

Read the full script

0:00Testing without looking

Polynomial identity testing asks whether an expression computes the zero polynomial. With commuting variables, substituting random numbers usually settles it. With noncommuting variables, numbers are not enough: x one times x two, minus x two times x one, is zero at every pair of numbers, yet it is a nonzero noncommutative polynomial. So one substitutes matrices. A formula here is a tree of additions and ordered multiplications whose leaves are variables or constants, and its size counts every vertex. A small formula can hide many words: the product of k copies of x one plus x two has 2^k of them. And a fixed small dimension cannot work: by the theorem of Amitsur and Levitzki, a certain 24-term polynomial in four variables vanishes on all 2-by-2 matrices. In our check, it vanished on 200 random integer examples, but not on a random 3-by-3 example. When the formula itself can be read, Raz and Shpilka gave a deterministic polynomial-time test, building on Nisan’s rank characterization. In the black-box setting, one may only evaluate. Bogdanov and Wee gave a randomized matrix test, and Forbes and Shpilka built deterministic hitting sets of quasipolynomial size over large enough fields. For formulas that may also invert, Arvind, Chatterjee and Mukhopadhyay gave quasipolynomial hitting sets. The goal is a list of polynomial size, or even a single point, built from the size bounds alone, before seeing the formula.

1:41The claims

Result 116 is three OpenAI preprints. The first, 13 pages, dated September 24, constructs in deterministic polynomial time one tuple of rational matrices, of dimension at most 2ns² for n variables and size s. Every nonzero formula of size at most s, over any field of characteristic zero, has a nonzero value there. So a single matrix evaluation decides whether a formula promised to be that small is zero. The second, 14 pages, dated October 4, does the same over every field of a given positive characteristic, including characteristic two, with matrices over the prime field of dimension of order n³s⁶. The third, 25 pages, dated September 24, treats rational formulas over the rationals, which may also take inverses. It builds a polynomial-size list of rational matrix tuples, so that every nonzero formula with some defined matrix evaluation has a defined, invertible value at one of them, with no bound on how deeply inverses are nested. For example, the inverse of x one x two minus x two x one is undefined at every pair of numbers, but defined at a pair of 2-by-2 matrices. OpenAI published Lean formalizations of the first and third papers; the positive-characteristic paper is not formalized. We have not run the Lean checks ourselves.

3:14How the proofs go

The characteristic-zero proof encodes each word as an iterated integral in one variable. The empty word gives the constant one, and putting letter i in front integrates the series divided by z plus i. These series are linearly independent, so a nonzero polynomial gives a nonzero series. The matrices are simply these integration operators acting on the first d Taylor coefficients; each entry is plus or minus one over r times a power of i. In our check, the series for all 63 words of length at most 5 in 2 letters were independent. How many coefficients are enough? A formula of size s has a path representation with at most 2s states, so its series is a component of a linear differential system with poles at minus one through minus n. Moura’s multiplicity estimate bounds how deeply a nonzero component of such a system can vanish at zero, whatever the coefficients, and that bound is below 2ns². So the first d coefficients already show it. In our check, 339 different random nonzero formulas of size up to 9 in 2 variables were all detected at the 324-dimensional tuple; none needed more than 6 coefficients. In positive characteristic this breaks: integration divides by whole numbers, differentiation kills pth powers, and the poles can collide. The second paper replaces the derivative by a multiplicative shift, z to t z, which divides by t^r − 1, never zero. A pole argument gives independence, a shifted Wronskian, whose leading term is a Vandermonde determinant, bounds the order of vanishing, and truncating powers of t yields matrices over the prime field. For inverses, a formula of size s yields at most s + 1 linear matrix pencils of order at most 2s + 1, and making them all invertible certifies every inverse gate and an invertible output. The list is built so that every such family of feasible pencils becomes invertible at one tuple, using a rank-expansion bound proved with a Wronskian, lifts into a division algebra, and a fixed integer grid of parameters. In our check, the commutator of two simple 2-by-2 matrices was diagonal with determinant −1, so its inverse is defined there.

5:43Where it stands

The preprints are not peer reviewed and have not been revised. The Lean formalizations check the hitting property of the explicit rational tuple, whose dimension, 2ns², is part of its definition; its construction cost is bounded only in the repository’s own cost model, outside the checked statement. They also check the hitting lists for rational formulas with their time and size bounds. The positive-characteristic paper is not formalized, and we have not run the checks. None of these papers is among those OSVerify reviewed, and we have seen no expert review. If they hold, then for each characteristic a single explicit matrix substitution of polynomial size tests every small noncommutative formula, and a polynomial list does the same for rational formulas over the rationals, improving the quasipolynomial constructions known before.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.