Agent-Based Proof Design via Lemma Flow Diagram
This addresses proof design for mathematical education, but appears incremental as it builds on existing concepts like flow proofs.
The paper tackles the problem of proof design and implementation by introducing Lemma Flow Diagram (LFD), an agent-based approach based on the multicut rule with shared cuts, which is described as modular, easy to use, read, and automate, offering an alternative to flow proofs in mathematical education.
We discuss an agent-based approach to proof design and implementation, which we call {\it Lemma Flow Diagram} (LFD). This approach is based on the multicut rule with $shared$ cuts. This approach is modular and easy to use, read and automate. Thus, we consider LFD an appealing alternative to `flow proof' which is popular in mathematical education. Some examples are provided.