Degree coverage with seven matrix multiplications
Let $\mathcal P_7 \subseteq \mathbb{C}[x]_{\le 128}$ be the set of polynomials obtained from $1$ and $x$ by arbitrarily many complex linear combinations of polynomials already computed and at most seven multiplications of two polynomials already computed: the $p$ for which $p(X)$ can be evaluated, for a square matrix $X$, with at most seven matrix–matrix multiplications. Identify $\mathbb{C}[x]_{\le 128}$ with $\mathbb{C}^{129}$ through the coefficients, and let $\overline{\mathcal P_7}$ be the Zariski closure of $\mathcal P_7$ there. Jarlebring and Lorentzon proved that $\mathcal P_7$ has dimension $49$, and that for four multiplications the corresponding maximum degree is $12$.
Problem. Is $$\max\{d \in \{0, \dots, 128\} : \mathbb{C}[x]_{\le d} \subseteq \overline{\mathcal P_7}\} = 42?$$
Source: Jarlebring and Lorentzon (2026), Conjecture 13.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- AG
- Keywords
- matrix multiplication, matrix polynomials, OpenProblemsInNLA
References
@article{jarlebring2026,
author = {Jarlebring, Elias and Lorentzon, Gustaf},
title = {The Polynomial Set Associated with a Fixed Number of Matrix-Matrix Multiplications},
journal = {SIAM J. Appl. Algebra Geom.},
volume = {10},
number = {3},
year = {2026},
pages = {549--581},
doi = {10.1137/25M1779036},
eprint = {2504.01500},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-mf14,
author = {Townsend, Alex},
title = {{MF-14}: Degree coverage with seven matrix multiplications},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/matrix-functions-and-stability/MF-14/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00094.
namespace RegistryProblems.OP_00094
noncomputable section
open Set Polynomial
abbrev Poly := Polynomial ℂ
abbrev CoefficientSpace := Fin 129 → ℂ
abbrev GatePolynomials := Fin 7 → Poly
/-- Available polynomials before zero-based gate `k`: initial `1, X` and
the outputs of strictly earlier multiplication gates. -/
def availableGenerators (q : GatePolynomials) (k : ℕ) : Set Poly :=
{1, X} ∪ {p | ∃ j : Fin 7, j.val < k ∧ p = q j}
def availableSpace (q : GatePolynomials) (k : ℕ) : Submodule ℂ Poly :=
Submodule.span ℂ (availableGenerators q k)
/-- Seven chronological multiplication gates. Free complex linear
combinations are represented by membership in the available vector space. -/
def IsSevenGateCircuit (q : GatePolynomials) : Prop :=
∀ k : Fin 7, ∃ u v : Poly,
u ∈ availableSpace q k.val ∧ v ∈ availableSpace q k.val ∧ q k = u * v
/-- Outputs after seven gates; circuits with fewer gates will be identified
with these by proving zero-gate padding, not by an assumed equivalence. -/
def IsSevenProductOutput (p : Poly) : Prop :=
∃ q : GatePolynomials, IsSevenGateCircuit q ∧ p ∈ availableSpace q 7
def coefficientVector (p : Poly) : CoefficientSpace :=
fun i => p.coeff i.val
def outputVectors : Set CoefficientSpace :=
coefficientVector '' {p | IsSevenProductOutput p}
/-- The exact canonical closure: simultaneous zero set of every complex
polynomial equation vanishing on the given set of full coefficient vectors. -/
def vanishingHull (S : Set CoefficientSpace) : Set CoefficientSpace :=
{z | ∀ F : MvPolynomial (Fin 129) ℂ,
(∀ w ∈ S, MvPolynomial.eval w F = 0) → MvPolynomial.eval z F = 0}
def sevenProductClosure : Set CoefficientSpace := vanishingHull outputVectors
/-- The full coefficient plane, including zero and all degrees below `d`. -/
def degreePlane (d : ℕ) : Set CoefficientSpace :=
{z | ∀ i : Fin 129, d < i.val → z i = 0}
def CoversDegree (d : ℕ) : Prop := degreePlane d ⊆ sevenProductClosure
def coveredDegrees : Set ℕ := {d | d ≤ 128 ∧ CoversDegree d}
/-- OP-00094: Degree coverage with seven matrix multiplications -/
def _root_.RegistryProblems.Problem_OP_00094 : Prop :=
IsGreatest coveredDegrees 42
end
end RegistryProblems.OP_00094
Formalised by George Stepaniants (Apache-2.0); reviewed by clemens-admin.
Available to match against in: Lean v4.33.1 with Mathlib v4.33.1.
Resolving this problem in Lean
Add the problems package as a dependency, import this problem's module, and prove the constant. Any published revision works.
In lakefile.toml:
[[require]] name = "RegistryProblems" git = "https://github.com/cthalhammer/registry-problems" rev = "753bebc58e3fee845f4fffec7d24e7c8cc2a689a"
In your proof:
import RegistryProblems.OP_00094 theorem resolution : RegistryProblems.Problem_OP_00094 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00094" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00094 := by sorry
You can also write the statement out in full; the verifier checks it matches up to definitional equality. Partial results and reductions are not matched against this statement.
Resolution claims
Seven chronological products cover every complex polynomial through degree 44 in the full 129-coefficient closure model, refuting the original equality 42. The later exact maximum 47 is outside this formalization. Local serial Lean, two nonauthor final reviews and two published-source Linux verification runs pass.
Starting from $1,x$ and allowing arbitrary complex linear combinations for free, we determine the largest degree whose entire coefficient space lies in the Zariski closure of outputs computable with seven products. The answer is $47$. A $49$-parameter polynomial family has a contact of order $47$ with a nonsingular $48$-variable coefficient differential, established by a contraction argument whose inequalities are checked …
Starting from $1,x$ and allowing free complex linear combinations, we prove that the Zariski closure of the polynomials computable with seven products contains every polynomial of degree at most $44$. This refutes the equality to $42$ conjectured by Jarlebring and Lorentzon for the largest such degree $d_7$. A simultaneous four-product degeneration retains two intermediate polynomials as well as an arbitrary …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, MF-14/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00094, "Degree coverage with seven matrix multiplications", clopen.solutions.