{"id":"palomar/PALOMAR-2026-10-08-000005","url":"https://github.com/selanavot/matrix-multiplication-all-fields/tree/8375e73ed454e3128500d10d87480c5dd597ff03","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-08-000005-v1.json","repo":"https://github.com/selanavot/matrix-multiplication-all-fields","tags":["cs.CC","cs.DS","msc:68Q17","msc:68W30","msc:15A69","matrix-multiplication","algebraic-complexity","lean-formalization"],"score":0,"title":"Matrix multiplication exponent at most 9/4 over arbitrary fields","trust":"high","domain":"cs.CC","source":"palomar","authors":["Sela Navot"],"reviews":0,"subject":"cs.CC","summary":"This development extends OpenAI's Lean proof of the matrix multiplication exponent bound 9/4 from the complex numbers to every field, including finite fields and fields of positive characteristic. It generalizes Fourier separation and interpolation over each field's algebraic closure, descends tensor powers through one fixed finite coefficient algebra, and connects the resulting exact-rank bounds to the original division-free arithmetic-program model. The compared statements include the arithmetic exponent upper bound, nonvacuity and lower-bound checks, an explicit positive-epsilon…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-10-08","reactions":{},"formalized":true,"formalizes":[{"title":"An Upper Bound of 9/4 for the Matrix Multiplication Exponent","identifier":"https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Matrix-Multiplication-Nine-Fourths-October-2-2026","relationship":"adapts"}]}