How to Prove Equations Using Diagrams - A Category Theorist Looks at E-Graphs

Explore the intersection of category theory and e-graphs in this Berkeley Seminar lecture that examines how diagrammatic reasoning can be used to prove equations. Delve into the operational semantics of e-graphs through a category-theoretic lens, discovering how these data structures, first invented in 1980, are gaining renewed attention for their power and adaptability in equational reasoning. Learn how classic category theory concepts, particularly diagrams and initial functors, provide a conceptual foundation for understanding the diagrammatic reasoning processes performed within e-graphs. Gain insights into work-in-progress research that bridges abstract mathematical theory with practical computational tools for equation solving and verification.