Open Research Index

LeanMMBound: the matrix multiplication exponent is below 2.3710449

Oliver Proudfoot, Andrew Perrault

Palomar Registrypalomar/PALOMAR-2026-10-07-000007Oct 7, 2026cs.CCscore 0

The matrix multiplication exponent ω is the least exponent such that n×n matrices can be multiplied in n^(ω+o(1)) operations. This repository proves in Lean 4 / Mathlib that ω < 2.3710449 over every commutative ring, improving the previous bound ω < 2.371177 (Dupont et al. 2026). ω is defined via the exact tensor rank of n×n matrix multiplication. The new ingredient is shared extraction across recursion levels of the asymmetric laser method. The formalization covers the full argument, from the Coppersmith–Winograd degeneration to an exact rational certificate checked in the Lean kernel. The…

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-10-07-000007
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-07-000007/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-07-000007/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'