← All papers
Graphical Rewriting for Diagrammatic Reasoning in Monoidal Categories in Lean4
cs.LO
Sep 1, 2024 · v1
TL;DR
Implements graphical rewriting for string diagram reasoning in monoidal categories in Lean 4.
Abstract
This paper presents a framework in Lean 4 for performing graphical rewriting in monoidal categories, enabling diagrammatic reasoning to be carried out within a formal proof assistant. The approach implements string diagram manipulation as rewriting rules, allowing proofs about monoidal categories to follow the intuitive graphical style used in mathematical practice.
Problem
Proofs about monoidal categories in formal proof assistants typically require algebraic manipulation of terms, whereas mathematicians reason diagrammatically using string diagrams. No prior framework in Lean 4 supported graphical rewriting for diagrammatic reasoning.
Approach
The framework implements string diagram manipulation as rewriting rules in Lean 4, allowing proofs about monoidal categories to follow the intuitive graphical style used in mathematical practice. Graphical rewriting is carried out within the proof assistant.
Results
A working framework in Lean 4 for performing graphical rewriting in monoidal categories, enabling diagrammatic reasoning to be carried out within a formal proof assistant.