Browse › Theoretical computer science › 116 Uniform black-box noncommutative identity testing across characteristics
One Rational Matrix Hitting Point for Noncommutative Formulas
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
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.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Formalization
- OpenAI math release, Uniform black-box noncommutative identity testing across characteristics: Lean scope notes (release Lean development, October 2026). The release's Lean formalization states the universal hitting property of one rational matrix tuple for nonzero division-free formulas over characteristic-zero fields (comparator statement
FormulaHitting.lean); per the scope note, the polynomial bit-construction bound and the $O(ns^2)$ dimension bound are not asserted in the formal statement. [family-level]
Related prior literature mentioned by others
- Michael A. Forbes and Amir Shpilka, Quasipolynomial-time Identity Testing of Non-Commutative and Read-Once Oblivious Algebraic Branching Programs (FOCS 2013; arXiv:1209.2408, revised 2013-09-22). VibeMathed's family entry identifies this quasipolynomial black-box hitting-set construction for noncommutative branching programs and division-free formulas as background to the family's claimed polynomial constructions. [family-level]
Possibly relevant literature (found by the agent, not checked)
- Shubham Bhardwaj and Ramprasad Saptharishi, Hitting Sets for Polynomials with Small Partial Derivative Spaces (arXiv:2609.34436, 2026-09-28). Its characteristic-zero hitting-set construction for commutative polynomials uses formal derivations and Wronskians, a possible methodological comparison with this paper's differential-system multiplicity argument. [AI-generated per source]
Elsewhere
- Emergent Mind: family 116
Independent sites; their content is not reviewed here.
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}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/116.md. The Lean statements have not been checked by people against the paper's claims.
Family 116: Uniform black-box noncommutative identity testing across characteristics
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.
Other papers in this family:
- Uniform Matrix Hitting Points in Every Positive Characteristic · October 4, 2026
- Polynomial Hitting Lists for Noncommutative Rational Formulas · September 24, 2026