we-solve (beta)

Math-108-A3 · revision r1 · on Math-108

OpenAI claim summary for Math-108

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 at unsolvedmath.com: partially solved. 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 stated arithmetic exponent bounds, including $9/4$ over the complex numbers, remain strictly above two. The requested exponent-two multiplication over the rational field is therefore not established, and arithmetic-operation estimates alone do not assert a bit-time implementation.

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

Manuscript

Contents
  1. Is the exponent of matrix multiplication 2
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Manuscript 1.
  5. Manuscript 2.
  6. Manuscript 3.
  7. Outline of the argument
  8. Formal verification
  9. Status caveat
  10. Sources

Is the exponent of matrix multiplication 2

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 107; 2026-09-24), the asserted result is that characteristic-zero matrix multiplication has square exponent below $2.258$, dual exponent above $0.465$, and rectangular exponent at aspect $0.709$ below $2.092$, with the stated finite-characteristic exceptions; In manuscript 2 (family 107; 2026-10-02), the asserted result is that the complex matrix-multiplication exponent is at most $9/4$; In manuscript 3 (family 107; 2026-09-24), the asserted result is that the square multiplication exponent is below $2.371054886006746$ over every fixed field, including every positive characteristic.

Mathematical statement of the claimed result

Manuscript 1.
In exact complex arithmetic, let $\omega$ be the square matrix-multiplication exponent, $w(k)$ the exponent for multiplying an $n\times n^k$ matrix by an $n^k\times n$ matrix, and $\alpha=\sup\{k:w(k)=2\}$. The claimed bounds are \[ \omega<1129/500=2.258,\qquad\alpha>0.465,\qquad w(0.709)<2.092. \] These are arithmetic exponents, rather than bit-complexity or finite-precision bounds.
Manuscript 2.
For every $\varepsilon>0$, the claim gives an exact complex-arithmetic algorithm multiplying two $n\times n$ matrices in \[ O_{\varepsilon}(n^{9/4+\varepsilon})\quad\text{operations},\qquad\omega\le9/4. \] Its associated tensor inequality uses $T=\sum_{i=1}^sT_i$ with every $T_i\ne0$, a shared first tensor factor and matched disjoint sectors on the other two. A tensor character $\lambda$ takes nonnegative real values and is additive, multiplicative and restriction-monotone, with $\lambda(1)=1$; define $p_X$ by $\lambda(x\sum_{j=1}^my_jz_j)=m^{p_X}$. For every probability vector $q$ the claimed inequality is \[ \lambda(T)\ge e^{p_XH(q)}\prod_i\lambda(T_i)^{q_i},\qquad H(q)=-\sum_iq_i\log q_i, \] with $0\log0=0$. These are exact arithmetic and tensor-character statements, without finite-precision assumptions.
Manuscript 3.
For every fixed field $F$, the claimed arithmetic exponent of square matrix multiplication satisfies \[ \omega_F<2.371054886006746<2.371054887. \] The exponent is the infimum of asymptotic powers achievable by exact field operations, allowing an arbitrarily small additive exponent slack. Positive and zero characteristics are both included.

Outline of the argument

For manuscript 1 (family 107; 2026-09-24), an auxiliary tensor supplies a conditional label to the missing third leg while retaining a dot-product block. Recursive completion trees and finite-family entropy optimization produce certified parameters; a strict comparison argument verifies the advertised boundaries.

For manuscript 2 (family 107; 2026-10-02), tensor degenerations separate blocks that already expose two independent variable legs. Character inequalities for polynomial multiplication, a determinant filtration, and discrete growth bound the detecting character values for matrix multiplication at the claimed exponent.

For manuscript 3 (family 107; 2026-09-24), a joint extraction from several tensor depths uses entropy and a common modular hash. Sequential deletion assigns variables compatibly, and exact integer tables repair inherited masks; the resulting direct sum is converted to an exponent bound by the rank comparison.

Formal verification

For manuscript 1 (family 107; 2026-09-24), the documented Lean scope is the stated matrix-multiplication exponent estimates over $\mathbb C$, including the rectangular bounds; the declarations do not extend these estimates to all characteristic-zero fields or the claimed finite-characteristic range.

The selected statement includes the clause used for this problem.

For manuscript 3 (family 107; 2026-09-24), OpenAI lists Lean statements for this assertion: the square multiplication exponent is below $2.371054886006746$ over every fixed field, including every positive characteristic.

The selected statement includes the clause used for this problem.

No Lean formalization is listed at this snapshot for manuscript 2 (family 107; 2026-10-02).

The linked family Comparator checks are MatrixFields.lean, MatrixMultiplication.lean.

Their named declarations include OAI.MatrixAllFields.MatrixMultiplication.AllFieldMain.omega_lt_source_constant, OAI.MatrixMultiplication.complex_alpha_gt_93_div_200, OAI.MatrixMultiplication.complex_omega_le_nine_quarters, OAI.MatrixMultiplication.complex_rectangular_omega_lt_523_div_250.

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