OpenAI's internal frontier model proved and formalized in Lean the main result of 'An Upper Bound of 9/4 for the Matrix Multiplication Exponent'. We prove that the exponent of matrix multiplication over the complex numbers is at most 9/4.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 107). The Lean development was not rebuilt locally.