Penrose diagrams in core Lean: a box is a matrix, a wire is an index, joining wires sums over it. The zig-zag, transpose, trace and sliding rules proved for every dimension and every matrix. MIT.
linear-algebra theorem-proving tenet tensor-networks string-diagrams lean4 lean-studio penrose-diagrams
-
Updated
Sep 28, 2026 - Lean