Using GPT-5 to prove new theorems on matrix multiplication (rybindmitry.github.io)

Dmitry Rybin reports that with help from LLMs (o3 for ideas and GPT-5 to construct proofs) he has proved new algebraic lower bounds for multiplying multiple matrices. For the smallest open case he shows that three 2×2 matrices require 14 scalar multiplications — i.e., the obvious sequential use of Strassen twice is optimal — and then generalizes: under a natural algorithm class (non‑commutative algorithms, no divisions, and homogeneity in each matrix’s entries) the minimal cost of multiplying k n×n matrices equals (k−1)·C(n,n). This closes a previously unstudied case and, if accepted, pins down a family of lower bounds in algebraic complexity of matrix multiplication. Technically, the work frames the problem via C(n,...,n) as the minimal count of scalar multiplications, leverages Strassen’s 7‑multiplication construction as baseline, and uses an LLM-suggested combinatorial/algebraic argument to rule out non-sequential shortcuts within the specified algorithm space. The result is significant because it reduces the search space for faster multi-matrix algorithms and demonstrates LLMs can assist in producing nontrivial, general proofs in algebraic complexity. Important caveats: the theorems depend on the stated algorithmic assumptions, so extensions to commutative settings or algorithms using divisions remain open; the community will need to review, formalize, and verify the GPT-5–assisted proofs.