See https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/AlphaEvolve.20Matmul.20Verification/with/519501658

def matmul4x4 (A B : Matrix (Fin 4) (Fin 4) ℂ) : Matrix (Fin 4) (Fin 4) ℂ

Equations

• matmul4x4 A B = ⋯ ⋯

theorem check (A B : Matrix (Fin 4) (Fin 4) ℂ) : matmul4x4 A B = A * B