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. (Lean)
Manuscripts (3)
Uniform Matrix Hitting Points in Every Positive Characteristic
October 4, 2026 · source · cite as \cite{OAI:Uniform-Matrix-Hitting-Points-in-Every-Positive-Characteristic-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.
One Rational Matrix Hitting Point for Noncommutative Formulas
September 24, 2026 · source · cite as \cite{OAI:One-Rational-Matrix-Hitting-Point-for-Noncommutative-Formulas-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.
Polynomial Hitting Lists for Noncommutative Rational Formulas
September 24, 2026 · source · Lean formalization available · cite as \cite{OAI:Polynomial-Hitting-Lists-for-Noncommutative-Rational-Formulas-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.
Result 116 · Theoretical computer science. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.
Source: https://github.com/openai/math/blob/main/CONTENTS.md