Diagrammatic Notations for Interactive Theorem Proving

Explore the potential of integrating visual aids into interactive theorem provers in this 29-minute conference talk from ACM SIGPLAN. Delve into the challenges of designing declarative languages for composable diagram templates that enhance the development and presentation of proofs. Learn how Shardul Chiplunkar and Clément Pit-Claudel address the gap between the ubiquity of diagrams in traditional mathematics and their scarcity in computerized mathematics. Discover approaches to creating good-looking implementations of common patterns and techniques for rapid prototyping of diagrams that remain stable across transformations and proof steps. Gain insights into enriching interactive theorem provers with on-the-fly visual aids that are both practical and user-friendly, potentially revolutionizing the way mathematicians interact with computerized proof systems.

[HATRA23] Diagrammatic notations for interactive theorem proving