Oct 6, 2026
Lean formalization in OpenAI math repository (Result 116)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Polynomial Hitting Lists for Noncommutative Rational Formulas'. 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.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 116). The Lean development was not rebuilt locally.