Oct 6, 2026
Lean formalization in OpenAI math repository (Result 107)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Complex Matrix Multiplication Below 2.258 and Rectangular Bounds'. — secondary writeup Over every field of characteristic zero, we prove that the square matrix-multiplication exponent satisfies ω < 2.258, the dual exponent satisfies α > 0.465, and \omega(1,0.709,1)\lt 2.092. The strict square and k = 0.709 rectangular bounds also hold over every field except possibly in one finite set of positive characteristics, in the arithmetic-operation model.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 107). The Lean development was not rebuilt locally.