Theoretical computer science · Result 116

Uniform black-box noncommutative identity testing across characteristics

3 papersLean

For each characteristic, constructs in deterministic polynomial bit time a polynomial-dimensional matrix tuple detecting every nonzero division-free noncommutative formula of bounded size over any field of that characteristic. Rational formulas over ℚ also admit polynomial-size hitting lists whenever they have a defined rational-matrix evaluation.

Watch

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation

▶The proposed solutionin preparation

Papers 3

Uniform Matrix Hitting Points in Every Positive Characteristic

OpenAI · October 4, 2026

We construct a single matrix substitution that detects every nonzero size-s division-free noncommutative formula in n variables over every field of a given positive characteristic. One deterministic machine, given a promised prime p in binary and n, s in unary, outputs matrices over 𝔽_p of dimension \(O(n^3s^6)\) in polynomial bit time. The same tuple works with arbitrary extension-field coefficients, including in characteristic two. The construction also applies to the stated acyclic algebraic path programs.

Read PDF Download Source

Cite

@misc{OAI:Uniform-Matrix-Hitting-Points-in-Every-Positive-Characteristic-October-4-2026,
  author = {{OpenAI}},
  title = {{Uniform Matrix Hitting Points in Every Positive Characteristic}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Uniform-Matrix-Hitting-Points-in-Every-Positive-Characteristic-October-4-2026/uniform-matrix-hitting-points-positive-characteristic.pdf}{OAI:Uniform-Matrix-Hitting-Points-in-Every-Positive-Characteristic-October-4-2026}},
  year = {2026}
}

One Rational Matrix Hitting Point for Noncommutative Formulas

OpenAI · September 24, 2026

We construct, in deterministic polynomial bit time, one tuple of rational matrices that detects every nonzero polynomial computed by a noncommutative division-free formula of a prescribed size. The matrices have dimension \(O(ns^2)\) for n variables and formula size s, and the same tuple works over every field of characteristic zero.

Read PDF Download Source

Cite

@misc{OAI:One-Rational-Matrix-Hitting-Point-for-Noncommutative-Formulas-September-24-2026,
  author = {{OpenAI}},
  title = {{One Rational Matrix Hitting Point for Noncommutative Formulas}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/One-Rational-Matrix-Hitting-Point-for-Noncommutative-Formulas-September-24-2026/One-Rational-Matrix-Hitting-Point-for-Noncommutative-Formulas-September-24-2026.pdf}{OAI:One-Rational-Matrix-Hitting-Point-for-Noncommutative-Formulas-September-24-2026}},
  year = {2026}
}

Polynomial Hitting Lists for Noncommutative Rational Formulas

OpenAI · September 24, 2026

We construct, in deterministic polynomial bit time, a polynomial-size list of rational matrix tuples for noncommutative rational formulas over ℚ of bounded tree size. Every nonzero admissible formula has a defined, invertible value at one tuple, with no separate bounds on inverse nesting or rational constant heights. Matrix dimensions, entry bit lengths, and total output length are polynomially bounded.

Read PDF Download Source

Cite

@misc{OAI:Polynomial-Hitting-Lists-for-Noncommutative-Rational-Formulas-September-24-2026,
  author = {{OpenAI}},
  title = {{Polynomial Hitting Lists for Noncommutative Rational Formulas}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Polynomial-Hitting-Lists-for-Noncommutative-Rational-Formulas-September-24-2026/Polynomial-Hitting-Lists-for-Noncommutative-Rational-Formulas-September-24-2026.pdf}{OAI:Polynomial-Hitting-Lists-for-Noncommutative-Rational-Formulas-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalization gives one explicit tuple of rational matrices that simultaneously detects every nonzero division-free noncommutative formula with at most \(s\) gates in \(n\) variables, for \(n,s\ge1\). Evaluation at that tuple is a nonzero matrix over every characteristic-zero field.

The selected theorem states this universal hitting property. The paper's deterministic polynomial bit-construction bound and matrix-dimension bound \(O(ns^2)\) are not separately asserted in it.

The formalized result constructs polynomial-size hitting lists for noncommutative rational formulas with rational constants, addition, multiplication, and inverse gates. Given the number of variables and a formula-size bound, one deterministic polynomial-time machine outputs rational matrix tuples of a common positive dimension. Every admissible nonzero formula within the size bound evaluates to an invertible matrix on some listed tuple. The matrix dimension, complete binary output length, and running time are all polynomially bounded.

Comparator links

Result	Comparator statement
One rational matrix tuple hitting all bounded-size noncommutative formulas	FormulaHitting.lean
Polynomial hitting lists for rational formulas	RationalHitting.lean

Scope note on GitHub →