{"id":"palomar/PALOMAR-2026-10-13-000009","url":"https://github.com/AIV5/mmrank21/tree/cb1557b7ea80ea66fae4714628663d8c1df7a48d","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-13-000009-v1.json","repo":"https://github.com/AIV5/mmrank21","tags":["cs.CC","math.RA","msc:68Q17","msc:15A69","msc:03B35","matrix-multiplication","bilinear-complexity","lean"],"score":0,"title":"A lower bound of 21 for 3 × 3 matrix multiplication over every field","trust":"high","domain":"cs.CC","source":"palomar","authors":["Andrey Ivanov"],"reviews":0,"subject":"cs.CC","summary":"Every exact bilinear algorithm for multiplying two 3 × 3 matrices over an arbitrary field uses at least 21 products of input linear forms. The theorem includes finite and infinite fields in every characteristic. The input linear forms and output matrices are unrestricted. This is a lower bound for exact bilinear complexity, not for border rank or general arithmetic circuits. The repository contains the proof development and an interface stated entirely with ordinary Mathlib matrices and linear maps.","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-10-13","reactions":{},"formalized":true}