{"version":1,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"mathlib","imports":["Mathlib.Data.Real.Basic","Mathlib.Tactic.Ring","Mathlib.Tactic.Linarith","Mathlib.Tactic.NormNum"],"statement_hash":"e42bdc53fe5923a5742d3ddc2f2009921c1ebcc1edf4f76f8467e4c19ca98258","problem":{"id":13,"title":"Matrix multiplication exponent two over the real numbers","description":"Prove that dense n×n matrix multiplication has real-arithmetic circuits of size O(n^(2+ε)) for every ε > 0. The fixed model permits real constants and addition, subtraction and multiplication gates, with n² outputs. The integer bound (gates.length+n²)^k ≤ C*n^(2*k+1), for every positive k and some C depending on k, expresses exponent two without real-power notation. Gates and output indices may depend on n, but not on the input matrices. Values are exact real numbers; floating-point approximation is not the target. Recent faster upper bounds, including the October 2026 preprint claiming 9/4, remain above the requested exponent two.\n\nResearch status checked 8 October 2026: no accepted general proof identified in the cited literature. This is a proposed formal statement; independent correspondence review is requested. A successful statement check establishes well-formedness, not the conjecture.","statement":"(fun run : List (Real ⊕ (Fin 3 × Nat × Nat)) → List Real → List Real =>\n  ∀ k : Nat, 1 ≤ k → ∃ C : Nat, 1 ≤ C ∧\n    ∀ n : Nat, 1 ≤ n →\n      ∃ gates : List (Real ⊕ (Fin 3 × Nat × Nat)),\n      ∃ outputs : Nat → Nat → Nat,\n        (gates.length + n ^ 2) ^ k ≤ C * n ^ (2 * k + 1) ∧\n        ∀ A B : Nat → Nat → Real, ∀ i j : Nat, i < n → j < n →\n          (run gates (((List.range (n ^ 2)).map (fun t => A (t / n) (t % n))) ++\n                      ((List.range (n ^ 2)).map (fun t => B (t / n) (t % n))))).getD (outputs i j) 0 =\n          (List.range n).foldl (fun acc t => acc + A i t * B t j) 0)\n(fun gates inputs => gates.foldl (fun values gate => values ++ [match gate with\n  | Sum.inl c => c\n  | Sum.inr op => if op.1.val = 0 then values.getD op.2.1 0 + values.getD op.2.2 0\n    else if op.1.val = 1 then values.getD op.2.1 0 - values.getD op.2.2 0\n    else values.getD op.2.1 0 * values.getD op.2.2 0]) inputs)","profile":"mathlib","module_pins":[],"module_context":[],"scope":{}},"source":"import Mathlib.Data.Real.Basic\nimport Mathlib.Tactic.Ring\nimport Mathlib.Tactic.Linarith\nimport Mathlib.Tactic.NormNum\n\ndef OA_statement : Prop := ((fun run : List (Real ⊕ (Fin 3 × Nat × Nat)) → List Real → List Real =>\n  ∀ k : Nat, 1 ≤ k → ∃ C : Nat, 1 ≤ C ∧\n    ∀ n : Nat, 1 ≤ n →\n      ∃ gates : List (Real ⊕ (Fin 3 × Nat × Nat)),\n      ∃ outputs : Nat → Nat → Nat,\n        (gates.length + n ^ 2) ^ k ≤ C * n ^ (2 * k + 1) ∧\n        ∀ A B : Nat → Nat → Real, ∀ i j : Nat, i < n → j < n →\n          (run gates (((List.range (n ^ 2)).map (fun t => A (t / n) (t % n))) ++\n                      ((List.range (n ^ 2)).map (fun t => B (t / n) (t % n))))).getD (outputs i j) 0 =\n          (List.range n).foldl (fun acc t => acc + A i t * B t j) 0)\n(fun gates inputs => gates.foldl (fun values gate => values ++ [match gate with\n  | Sum.inl c => c\n  | Sum.inr op => if op.1.val = 0 then values.getD op.2.1 0 + values.getD op.2.2 0\n    else if op.1.val = 1 then values.getD op.2.1 0 - values.getD op.2.2 0\n    else values.getD op.2.1 0 * values.getD op.2.2 0]) inputs))\n\n#check OA_statement\n","proof":null}