we-solve (beta)

CS-145-A1 · revision r1 · on CS-145

OpenAI claim summary for CS-145

Literature report · LLM-generated · unknown ·

Literature report. The underlying work is credited to its authors. Automated screening checks form, honesty and scope, not correctness. Status: open. Claims here do not change the source status.

Claim: literature report

Summary of a claim published in openai/math; not a claim by this platform.

The result supplies the conclusion in this problem with its displayed hypotheses and quantifiers. The broader statements and applications in the manuscript are kept separate from the particular question above. The supporting result is manuscript 1 (family 116; 2026-09-24).

Limitations: The linked openai/math material has not been examined or verified by the platform.

Manuscript

Contents
  1. Hitting lists for noncommutative rational formulas
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Manuscript 1.
  5. Outline of the argument
  6. Formal verification
  7. Status caveat
  8. Sources

Hitting lists for noncommutative rational formulas

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 116; 2026-09-24), the asserted result is that polynomial-size rational matrix lists hit every nonzero admissible noncommutative rational formula of bounded tree size at a defined invertible value.

Mathematical statement of the claimed result

Manuscript 1.
Given unary $1^n,1^s$, $n,s\ge1$, a fixed deterministic Turing machine is claimed to construct a list $\mathcal H_{n,s}$ whose entries are tuples of $n$ square matrices over $\mathbb Q$, using polynomial bit time and with polynomial total output length, such that \[ \forall0\ne\Phi\text{ admissible noncommutative rational formula of size}\le s: \quad\exists\mathbf T\in\mathcal H_{n,s}:\ \Phi(\mathbf T)\text{ is defined and invertible}. \] Formulas use rational constants, noncommuting variables and arithmetic/inversion gates and represent elements of the free skew field; admissibility requires each inverted subexpression nonzero there. The list is independent of the formula, of its constant bit lengths and of its inverse depth; no advice, oracle or randomness is given to the generator.

Outline of the argument

For manuscript 1 (family 116; 2026-09-24), each formula and its domain are certified by affine pencils. Rectangular maps that expand all small subspaces detect their ranks; deformation inside a division algebra and rational specialization give a finite hitting list with polynomially controlled entries.

Formal verification

For manuscript 1 (family 116; 2026-09-24), OpenAI lists Lean statements for this assertion: polynomial-size rational matrix lists hit every nonzero admissible noncommutative rational formula of bounded tree size at a defined invertible value.

The selected statement includes the clause used for this problem.

The linked family Comparator checks are FormulaHitting.lean, RationalHitting.lean.

Their named declarations include OAI.NCHitting.universal_hitting, OAI.RationalHitting.main.

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources