Extending the Lean User Interface with Widgets - A Tutorial

Explore the potential of extending the Lean 4 editor environment with custom widgets in this 32-minute tutorial talk. Discover how to enhance formal mathematics communication by incorporating visual elements into proofs, particularly geometric aspects often lost in traditional formal presentations. Learn to create interactive tools for better understanding proof automation and utilizing proof assistants as computational environments similar to Jupyter notebooks. Follow along as the speaker demonstrates the process of developing a simple widget to visualize mathematical objects and, time permitting, shows how to interactively trace tactic execution. Gain insights into improving mathematical communication, automating proofs, and leveraging Lean 4's extensibility to create more intuitive and interactive formal mathematics experiences.