Uniform black-box noncommutative identity testing across characteristics

One fixed set of matrices exposes every nonzero small formula whose variables do not commute.

3 papers September 24, 2026 Explained by AI

Some expressions look like zero for ordinary numbers but not for matrices, where multiplication order matters. These papers build matrices in advance that catch every nonzero formula up to a given size. One paper proves that a single tuple of fraction matrices works over every characteristic-zero field (Lean proof listed). A second proves that a short list handles formulas with division (Lean proof listed). A third claims to prove that one tuple works in each prime characteristic too.

First step

2005

Ran Raz and Amir Shpilka, a deterministic test that reads the formula

Significance

Major

It replaces quasipolynomial-size hitting sets with polynomial ones for formulas, with and without division.

Trust

Formal proof listed

Field

Theoretical computer science

3 papers

The explanation

Take the expression x·y − y·x. Put in any two ordinary numbers and you get 0, because 3·5 equals 5·3. Now put in two small grids of numbers called matrices. Let X have rows (0, 1) and (0, 0). Let Y have rows (0, 0) and (1, 0). Then X·Y has rows (1, 0) and (0, 0). But Y·X has rows (0, 0) and (0, 1). Their difference has rows (1, 0) and (0, −1), which is not zero. Matrices can expose an expression that ordinary numbers make look like zero.

Matrices do this because their order of multiplication matters. Variables whose order matters are called noncommutative. A noncommutative formula builds an expression from variables and numbers using only addition and multiplication, arranged as a tree. Its size counts every piece of the tree, numbers and variables included. The basic question is identity testing: does a given formula compute zero once everything is multiplied out?

These papers ask for the hardest version of that test. You may not look inside the formula. You may only plug matrices in and see the result. Worse, you must choose the matrices in advance, knowing only the number of variables and a size limit. A hitting point is one fixed choice that gives a nonzero answer for every nonzero formula within those limits. A hitting list is a short list of choices where at least one works.

The obstacle is that a small formula can hide a huge expression. Multiply x₁ + x₂ by itself 10 times, keeping the order. The formula has 39 pieces. Multiplied out, it has 1024 different words, such as x₁x₂x₂x₁… in every order. A fixed set of matrices must keep all of them from cancelling, for every formula, without seeing any of them.

Earlier work left a gap. Ran Raz and Amir Shpilka gave a fast exact test in 2005, but it needs to read the formula. Andrej Bogdanov and Hoeteck Wee gave a test that only plugs in matrices, but it relies on random choices. In 2013, Michael Forbes and Amir Shpilka built fixed hitting sets without randomness. Their sets have quasipolynomial size, which grows faster than any fixed power of the formula size. In 2026, Foram Lakhani and Partha Mukhopadhyay built one fixed matrix tuple for sparse expressions, those with few words. A small formula can have very many words, as the example showsSource 1.

The first paper proves that one fixed tuple is enough over the rational numbers (fractions). For n variables and size limit s, the paper also claims at most 2ns² rowsSource 2. It claims a build time that grows like a fixed power of n and sSource 2. The same tuple works over every number system where no whole number other than 0 equals zeroSource 3. For the example, n = 2 and s = 39, so 6084 rows suffice. The idea is to turn each word into its own distinct infinite list of numbersSource 4. A small formula's list cannot begin with too many zeros, so a finite window of the list is enoughSource 5.

The second Lean-checked paper handles division. A rational formula may also invert a matrix, which only works when that matrix is invertible. It proves a polynomial-size list of fraction-valued matrix tuples for such formulas with fraction constants. Every nonzero formula with some defined matrix value gets a defined, invertible value on some listed tupleSource 6. This holds however deeply inverses nest and however large the constants areSource 7. Earlier hitting sets of V. Arvind, Abhranil Chatterjee and Partha Mukhopadhyay had quasipolynomial size.

The third paper moves to characteristic p, for a prime p. There, adding p copies of 1 gives 0. The fraction method breaks there. It divides by whole numbers, and dividing by p is impossible thereSource 8. Slopes also fail: when p = 2, the slope of z² is 2z, which is 0. The paper replaces slopes with a shift that multiplies z by a new symbolSource 9. It claims to prove that one tuple works in each characteristic p, including p = 2Source 10. Its matrices have on the order of n³s⁶ rows, more than in the fraction case. It is built in time polynomial in n, s and the number of digits of pSource 11.

These results do not say formulas can be evaluated quickly. The time bounds cover building the matrices, not plugging in an unknown formulaSource 12. The first paper asserts no bound for circuits that reuse shared piecesSource 13. How sure is this? A computer proof checker called Lean has checked two statements. One is that a single fraction-valued tuple hits every nonzero formula of size at most s. That Lean statement does not include the 2ns² row bound or the time bound. The other is the full hitting-list theorem for formulas with division, including its polynomial bounds. The characteristic p paper is outside the Lean scope note. No specialist review has been published.

What it doesn't show. This does not cover general circuits that reuse shared pieces, and it does not make evaluating an unknown formula fast.

Where it came from

This result comes from an unreleased OpenAI model, published in the openai/math release on 6 October 2026.

Hype check

Major if the proofs hold. Lean has checked the single-tuple hitting property and the division hitting-list theorem. The single tuple's size and time bounds and the whole characteristic p paper are not in that check. No specialist review has been published.

Words used

Matrix: A square grid of numbers that can be added and multiplied; the order of multiplication matters.
Noncommutative: Describes variables where x times y need not equal y times x.
Formula: An expression built as a tree of additions and multiplications, with no shared pieces.
Identity testing: Deciding whether an expression computes zero once everything is multiplied out.
Hitting point: One fixed choice of matrices that gives a nonzero answer for every nonzero formula in a class.
Quasipolynomial: Growing faster than any fixed power of the input size, but much slower than exponential growth.
Characteristic: The number of copies of 1 that add to 0 in a number system; 0 if none do.
Lean: A computer program that checks mathematical proofs step by step.

The original papers (3)

Uniform Matrix Hitting Points in Every Positive Characteristic (PDF, opens in a new tab)
October 4, 2026
One Rational Matrix Hitting Point for Noncommutative Formulas (PDF, opens in a new tab)
September 24, 2026
Polynomial Hitting Lists for Noncommutative Rational Formulas (PDF, opens in a new tab)
September 24, 2026 Formal proof listed

Lean notes

All quoted lines (13)

The obstacle is that a small formula may contain exponentially many words after expansion.
One Rational Matrix Hitting Point for Noncommutative Formulas Back to text
There is a deterministic algorithm which, given integers $n,s\ge1$ , constructs a tuple $\mathbf T_{n,s}\in\Mat_d(\Q)^n, \qquad d\le 2ns^2,$ in time polynomial in $n,s$ , measured in bit operations. The numerators and denominators of its entries have bit length $O(\log(ns+1)+ns^2\log(n+1))$ .
One Rational Matrix Hitting Point for Noncommutative Formulas Back to text
For every field $F$ of characteristic zero and every $0\ne f\in\mathsf{Form}_{n,s}(F)$ , $f(\mathbf T_{n,s})\ne0,$ where the tuple is viewed over $F$ through the canonical embedding $\Q\hookrightarrow F$ .
One Rational Matrix Hitting Point for Noncommutative Formulas Back to text
We encode words by iterated integrals in one variable.
One Rational Matrix Hitting Point for Noncommutative Formulas Back to text
Linear independence makes $h_f$ nonzero, and the order bound ensures that this finite truncation retains a nonzero coefficient.
One Rational Matrix Hitting Point for Noncommutative Formulas Back to text
some tuple in … is a defined evaluation of … with invertible value
Polynomial Hitting Lists for Noncommutative Rational Formulas Back to text
The same list works for all such formulas, regardless of the bit lengths of their rational constants or their inverse depth.
Polynomial Hitting Lists for Noncommutative Rational Formulas Back to text
The analytic-looking part of the construction is not: formal integration divides by positive integers, ordinary differentiation annihilates $p$ th powers in characteristic $p$ , and distinct integer pole locations may coincide.
Uniform Matrix Hitting Points in Every Positive Characteristic Back to text
We retain the word-series and matrix-system organization, replacing the differential operator by an infinite-order multiplicative shift.
Uniform Matrix Hitting Points in Every Positive Characteristic Back to text
In particular, its guarantee is uniform over arbitrary extensions of $\F_p$ , and applies to $p=2$ without any relation between the characteristic and the formula size.
Uniform Matrix Hitting Points in Every Positive Characteristic Back to text
These results provide relevant benchmarks, while the construction here is polynomial in formula size and in the binary length of the characteristic.
Uniform Matrix Hitting Points in Every Positive Characteristic Back to text
The time to evaluate a formula over an unspecified coefficient field is separate from the bit complexity of constructing the tuple.
Uniform Matrix Hitting Points in Every Positive Characteristic Back to text
No bound for arbitrary shared circuits is asserted.
One Rational Matrix Hitting Point for Noncommutative Formulas Back to text