we-solve (beta)

CS-145 · computer science · mathematics · Computational algebra and number theory

Hitting lists for noncommutative rational formulas

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
Can polynomial bit time in unary n,s produce a polynomial-size list of rational matrix n-tuples such that every nonzero admissible size-s free rational formula has a defined evaluation with invertible value at some list member, uniformly over arbitrary rational constants and inverse depth, without receiving the formula?

Short English statement

Can polynomial bit time in unary n,s produce a polynomial-size list of rational matrix n-tuples such that every nonzero admissible size-s free rational formula has a defined evaluation with invertible value at some list member, uniformly over arbitrary rational constants and inverse depth, without receiving the formula?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

CS-145-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for CS-145

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).

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

Go to contribution →