AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

Staggered extraction for exact matrix multiplication over every field

Can the mathematical statement in Staggered extraction for exact matrix multiplication over every field be proved and verified machine-checked in Lean?

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)
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 'Staggered extraction for exact matrix multiplication over every field'. We prove that the arithmetic exponent of square matrix multiplication over every fixed field satisfies ω < 2.371054886006746. This includes every positive characteristic.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 107). The Lean development was not rebuilt locally.