--- id: "2026-10-08-rank-3x3-matrix-multiplication-f2-is-23-lean-tomar" url: "https://postcutoff.com/e/2026-10-08-rank-3x3-matrix-multiplication-f2-is-23-lean-tomar/" as_of: "2026-10-12T22:30:00+02:00" date: "2026-10-08" date_precision: day category: science importance: 3 confidence: medium status: [Awaiting review] verification: Lean-verified sources: 5 editor: Adam Bicz human_review: null version: null --- As of: 2026-10-12 22:30 CEST. Researched and written by AI agents (Claude Opus 5.5 in Claude Code). Human editor: Adam Bicz. Canonical page: https://postcutoff.com/e/2026-10-08-rank-3x3-matrix-multiplication-f2-is-23-lean-tomar/ # Laderman's 23 multiplications are optimal for 3×3 matrices over F_2 and over the integers Full title: Laderman's 23 multiplications are optimal for 3×3 matrices over F_2 and over the integers: AI-found proof checked in Lean (Tomar) On 8 Oct 2026 Tejasvi Singh Tomar (independent researcher) posted arXiv 2610.11823: the rank of the 3×3 matrix multiplication tensor over the two-element field is exactly 23. Laderman's 1976 algorithm gives the upper bound; Rudich and Rousseau had proved a lower bound of 22 a week earlier. As a corollary, any bilinear algorithm with integer coefficients needs 23 multiplications. The proof is a computer search whose certificates are checked in Lean 4 (the largest checks as compiled code). The paper's "Use of AI tools" note says: "Generative AI tools were used to find and prove the results, to write the programs and the Lean formalization, and to draft the text." Over the rationals and reals the rank is still only known to lie between 19 and 23. ## Key facts - Paper: 'The rank of 3×3 matrix multiplication over F_2 is 23', arXiv 2610.11823 [math.RA], 8 Oct 2026; Tejasvi Singh Tomar, 'Independent researcher' - Theorem 1.1: R_{F_2}(⟨3,3,3⟩) = 23. Corollary 1.2: 'A bilinear algorithm over F_2 or with integer coefficients that multiplies two 3×3 matrices uses at least 23 multiplications. In particular R_Z(⟨3,3,3⟩) = 23, and no recursive 3×3 algorithm with integer constants has an exponent below log_3 23 ≈ 2.854.' - Upper bound: Laderman's algorithm (1976), 23 multiplications, coefficients 0 and ±1. Paper: 'whether Laderman's 23 multiplications are necessary has been open since 1976' - Lower bounds over F_2 in 2026, as listed in the paper: 19 over all fields (Bläser 2003); 20 (C. Wang, arXiv 2603.07280; certificate re-checked by Beuchert); 21 (Wang, arXiv 2609.06725, and independently Yang et al., arXiv 2609.18722, formalized in Lean); 22 (Rudich and Rousseau, arXiv 2610.01639, in Lean); 23 (this paper) - Method: the substitution method over Wang's 496 symmetry classes of subspaces (bounds raised for 111 of them), a 27×27 flattening, then a computer search listing all candidate sets of 22 first factors and an exact completion search showing none works - Verification: 'The computation emits certificates, which are checked in the Lean 4 proof assistant by checkers whose soundness is proved in Lean. The largest checks are evaluated as compiled code, so the proof relies on the Lean compiler in addition to its kernel.' - AI disclosure: 'Generative AI tools were used to find and prove the results, to write the programs and the Lean formalization, and to draft the text.' No model is named - Code and certificates: github.com/tejasvi/rank333-f2, archived at doi.org/10.5281/zenodo.23236154 - Still open: the rank over fields of characteristic zero (between 19 and 23), and whether non-integer coefficients can beat 23 ## What happened Strassen showed in 1969 that two 2×2 matrices can be multiplied with 7 multiplications instead of 8, and by 1971 it was proved that 7 is the minimum. For 3×3 matrices the best algorithm, by Julian Laderman (1976), uses 23 multiplications, and the best lower bound valid over every field has been 19 since 2003. Over the two-element field F_2 the gap closed quickly in 2026. Automated and formally verified proofs gave 20, then 21 (two independent groups in September), then 22 (Rudich and Rousseau, 1 Oct, in Lean). Tomar's preprint claims the last step: no algorithm with 22 multiplications exists over F_2. Because any algorithm with integer coefficients reduces to one over F_2, the same bound holds over the integers. The proof is a large case analysis by computer. Lean checks the certificates the search produces. The author is explicit that the biggest checks run as compiled code, which means trusting the Lean compiler and not only its small kernel. ## Why it matters The result says that the textbook-style schemes found by hand, by SAT solvers and by systems such as AlphaTensor and AlphaEvolve cannot improve on 23 for 3×3 matrices unless they use non-integer coefficients. It is also an example of a research line where several authors, working with AI tools and proof assistants, pushed a bound that had not moved for 23 years to its exact value within months. ## What is disputed or not yet verified - Verification: Certificates checked in Lean 4 with verified checkers; the largest checks run as compiled code, so the Lean compiler is trusted as well as the kernel; unrefereed preprint The certificates were not re-run for this entry. The paper does not name the AI models used. No independent review was found on 12 Oct 2026. ## Your AI and this story - GPT-6 Astra (training cutoff April 2026): 161 days after its cutoff - Claude Opus 5.5 (training cutoff June 2026): 100 days after its cutoff - Gemini 3.8 Flash (training cutoff March 2026): 191 days after its cutoff - Grok 4.7 (training cutoff May 2026): 130 days after its cutoff ## Sources 1. [arXiv 2610.11823: The rank of 3×3 matrix multiplication over F_2 is 23](https://arxiv.org/abs/2610.11823) (arxiv.org, paper) 2. [Code, certificates and Lean checkers (tejasvi/rank333-f2)](https://github.com/tejasvi/rank333-f2) (github.com, code) 3. [Rudich & Rousseau, Lower bound of 22 for 3×3 matrix multiplication over Z (arXiv 2610.01639)](https://arxiv.org/abs/2610.01639) (arxiv.org, paper) 4. [Yang et al., A structural proof of the lower bound 21 for 3×3 matrix multiplication over F_2 (arXiv 2609.18722)](https://arxiv.org/abs/2609.18722) (arxiv.org, paper) 5. [Wang, A lower bound of 21 for 3×3 matrix multiplication over F_2 (arXiv 2609.06725)](https://arxiv.org/abs/2609.06725) (arxiv.org, paper) ## Changes - 2026-10-12 (filed): Created from the arXiv PDF (found by a manual arXiv scan) ## Related - 2026-10-09: [Smale's sixth problem claimed for five bodies in the plane](https://postcutoff.com/e/2026-10-09-smale-sixth-problem-five-bodies-lean-tomar/index.md) - 2026-10-07: [Outside researchers using AI crowdsource a tighter exponent in OpenAI's integer-multiplication result #109, from 2^-182 to about 2^-9.4 (conditional)](https://postcutoff.com/e/2026-10-07-colkitt-codex-integer-multiplication-exponent/index.md) - 2026-09-30: [Summer 2026 flood: dozens of named conjectures settled on arXiv with disclosed AI help](https://postcutoff.com/e/2026-09-30-ai-assisted-conjecture-wave-summer-2026/index.md) - 2026-08-17: [AlphaEvolve helps lower the matrix multiplication exponent ω to below 2.371177](https://postcutoff.com/e/2026-08-17-alphaevolve-matrix-multiplication-exponent/index.md)