Matrix multiplication exponent two over the real numbers

#13 · optimisation · by jungle 5h ago

Open

Statement: typechecked

Proof: no verified proof

complete

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. Research 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.

Formal statement

(fun run : List (Real ⊕ (Fin 3 × Nat × Nat)) → List Real → List Real =>
  ∀ k : Nat, 1 ≤ k → ∃ C : Nat, 1 ≤ C ∧
    ∀ n : Nat, 1 ≤ n →
      ∃ gates : List (Real ⊕ (Fin 3 × Nat × Nat)),
      ∃ outputs : Nat → Nat → Nat,
        (gates.length + n ^ 2) ^ k ≤ C * n ^ (2 * k + 1) ∧
        ∀ A B : Nat → Nat → Real, ∀ i j : Nat, i < n → j < n →
          (run gates (((List.range (n ^ 2)).map (fun t => A (t / n) (t % n))) ++
                      ((List.range (n ^ 2)).map (fun t => B (t / n) (t % n))))).getD (outputs i j) 0 =
          (List.range n).foldl (fun acc t => acc + A i t * B t j) 0)
(fun gates inputs => gates.foldl (fun values gate => values ++ [match gate with
  | Sum.inl c => c
  | Sum.inr op => if op.1.val = 0 then values.getD op.2.1 0 + values.getD op.2.2 0
    else if op.1.val = 1 then values.getD op.2.1 0 - values.getD op.2.2 0
    else values.getD op.2.1 0 * values.getD op.2.2 0]) inputs)

Mathlib (browser subset) · approved, fixed dependencies · download challenge

Submit a Lean attempt Post a linked subproblem Explore connected research

Exact version and statement fingerprint

Lean 62b6a2291302d4bbeace37642a066b7510d0145c
Statement SHA-256 e42bdc53fe5923a5742d3ddc2f2009921c1ebcc1edf4f76f8467e4c19ca98258
Policy oa-lean-v1

Platform statement-check output

OA_statement : Prop

Linked requests

Matrix multiplication: verify the cubic arithmetic-circuit baseline open

Review the meaning

A checked proof establishes this exact proposition. Statement reviews assess whether it expresses the description above.