Black-box identity testing for noncommutative formulas

Black-box identity testing for noncommutative formulas asks for matrix substitutions, chosen in advance from size bounds alone, that detect whether a noncommutative arithmetic formula computes a nonzero polynomial or rational function. Three manuscripts in OpenAI's public mathematics collection (github.com/openai/math) claim:

• a single explicit tuple of rational matrices of polynomial dimension for division-free formulas over every field of characteristic zero;
• a single tuple over the prime field for every positive characteristic;
• polynomial-size hitting lists for rational formulas, with inverse gates, over the rational numbers.

Two of the results are formalized in Lean. This page summarizes the published claims 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 introductions of the manuscripts:
  • A noncommutative formula is a tree of addition and ordered multiplication gates over variables and scalars. Its value at a tuple of square matrices is the matrix obtained by substitution. A hitting point for a class of polynomials is one tuple at which every nonzero member has nonzero value, and a hitting set allows several tuples.
  • Nisan characterized branching-program complexity by ranks of coefficient matrices. Raz and Shpilka gave deterministic polynomial-time identity tests for noncommutative formulas and algebraic branching programs with access to the input (the white-box model). Bogdanov and Wee gave a randomized black-box test by matrix evaluation. Forbes and Shpilka constructed deterministic quasipolynomial-size matrix hitting sets for noncommutative algebraic branching programs over sufficiently large fields.
  • For formulas with inverse gates, Hrubeš and Wigderson developed the rational-formula model and its reduction to singularity testing of linear matrices over the free skew field. Deterministic polynomial-time white-box algorithms followed from operator scaling (Garg, Gurvits, Oliveira and Wigderson) and from constructive noncommutative-rank computation (Ivanyos, Qiao and Subrahmanyam). Derksen and Makam gave polynomial dimension bounds and a randomized black-box test. Arvind, Chatterjee and Mukhopadhyay obtained deterministic quasipolynomial-size hitting sets, first for rational formulas of inversion height two and then for unrestricted rational formulas, over the rationals.
  • Lakhani and Mukhopadhyay constructed one integer matrix tuple for sparse noncommutative polynomials over characteristic-zero fields, and Lakhani and Saxena gave randomized black-box tests for homogeneous constant-depth circuits.

The original results

• Claim (characteristic zero). Theorem 1.1 of One Rational Matrix Hitting Point for Noncommutative Formulas states that a deterministic algorithm constructs, in time polynomial in n and s, one tuple of n rational matrices of dimension at most 2ns². Its entries have polynomially bounded bit length, and it detects every nonzero division-free noncommutative formula of size at most s in n variables over every field of characteristic zero. The manuscript states that the same construction applies to acyclic algebraic branching programs with m vertices, with matrix dimension (n − 1)m(m − 1)/2 + m, and that this improves the preceding quasipolynomial hitting-set bound in characteristic zero.
• Method, as described: words are encoded by iterated integrals in one variable, whose linear independence the manuscript proves directly. A formula is converted to a small acyclic path representation, and an order-of-vanishing bound justifies truncating the encoding.
• Claim (positive characteristic). Theorem 1.1 of Uniform Matrix Hitting Points in Every Positive Characteristic states that a deterministic machine, given a prime p in binary and n, s in unary, outputs one tuple of matrices over the prime field of dimension O(n³s⁶) in polynomial time. The tuple detects every nonzero division-free formula of size at most s over every field of characteristic p, including characteristic two.
• Method, as described: the manuscript keeps the word-series organization of the characteristic-zero companion, replaces the differential operator by a multiplicative shift, proves the resulting order bound in the given characteristic, and descends to prime-field matrices by truncating a power series in an auxiliary variable.
• Claim (rational formulas). Theorem 1.1 of Polynomial Hitting Lists for Noncommutative Rational Formulas states that a deterministic machine, given n and s in unary, outputs in polynomial time a list of tuples of rational square matrices. For every nonzero admissible rational formula of size at most s with rational constants, some listed tuple gives a defined evaluation with invertible value. The list does not depend on the bit lengths of the constants or on the nesting of inverses.
  • The manuscript states that this resolves, over the rationals, the explicit polynomial-size hitting-set problem for this formula model, and gives the polynomial matrix dimension asked for in the conclusion of Arvind, Chatterjee and Mukhopadhyay.
  • Corollaries state that the construction hits every feasible rational affine linear pencil of bounded order, answering the rational-coefficient version of a black-box construction question for the singularity of homogeneous pencils posed by Garg, Gurvits, Oliveira and Wigderson. Another corollary gives a universal list that recovers the noncommutative rank of rectangular rational pencils.
• Method, as described: rectangular test matrices built from Taylor expansions about distinct points give a subspace-expansion property by a Wronskian bound. A lift into a division algebra forces full rank, and representing the auxiliary parameters by rational matrices and an integer grid makes the list explicit.
• Sources. The manuscripts:
  • One Rational Matrix Hitting Point for Noncommutative Formulas (24 September 2026);
  • Polynomial Hitting Lists for Noncommutative Rational Formulas (24 September 2026);
  • Uniform Matrix Hitting Points in Every Positive Characteristic (4 October 2026).
• Formalization, as described by the repository. The scope note lean/docs/116.md lists the first two manuscripts.
  • It states that the formalization gives one explicit tuple of rational matrices on which every nonzero division-free formula of the size bound is nonzero over every characteristic-zero field, and that the deterministic bit-construction bound and the dimension bound are not separately asserted.
  • It also states that the formalization constructs polynomial-size hitting lists for rational formulas with rational constants, with polynomially bounded matrix dimension, output length and running time.
  • The Comparator statements are FormulaHitting.lean and RationalHitting.lean. The positive-characteristic manuscript is not listed in the scope note.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 19 October 2026)
2026-10-08	MathVet (GitHub, review of openai/math, tables at repository commit bb5fdb6, 18 October 2026)	Review (fidelity of the formal statements)	Rates the family "partial". The characteristic-zero existence of one hitting tuple and the polynomial-time rational hitting lists are stated in Lean; the positive-characteristic construction and the polynomial bit-time bound for the single tuple are not. It notes that the hitting property quantifies over admissible formulas through a relational evaluation in which an inverse requires an actual two-sided inverse, and that the machine model takes unary input. It records sandboxed Comparator passes for both challenges.	MathVet states that its ratings concern whether the Lean states the headline claims.
2026-10-10	cert-machine, openai/math lane K, runs 38019899278 (FormulaHitting) and 38040214623 (RationalHitting)	Verification (kernel replay)	Records that Lean's default kernel and the nanoda kernel both accept both solutions.	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 lists neither FormulaHitting nor RationalHitting, so both were accepted by con-leche and by Lean's official kernel.	Development journal.
2026-10-16	J. Jardine, Lattice24, referee reviews rank_526 (characteristic-zero hitting point) and rank_539 (positive characteristic) in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995)	Review (AI-assisted audit)	Both reviews report no gap; the reviewer states that it read both manuscripts in full and lists the steps it checked.	Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0.

Notes

• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.