← All papers
An Extensible User Interface for Lean 4
cs.LO
Jul 26, 2023 · v1
TL;DR
Introduces ProofWidgets 4, an extensible UI framework built into the core Lean 4 distribution.
Abstract
Modern proof assistants handle complex automation and large libraries, but understanding the emergent interactions between components can be a serious challenge. This paper proposes presentations, UI elements that store references to the objects they are displaying, as a productive framework for ITP interface design. The authors built an extensible user interface for Lean 4 with the ProofWidgets 4 library, demonstrating examples including type information popups, structured traces, contextual suggestions, algebraic reasoning displays, and red-black tree visualizations. The interface is already part of the core Lean distribution.
Problem
Modern proof assistants handle complex automation and large libraries, but understanding the emergent interactions between components through the user interface remains a challenge.
Approach
The authors propose presentations as a UI framework: UI elements that store references to the objects they display. They built an extensible user interface for Lean 4 with the ProofWidgets 4 library, demonstrating type information popups, structured traces, contextual suggestions, algebraic reasoning displays, and red-black tree visualizations.
Results
The ProofWidgets 4 library is now part of the core Lean distribution, providing an extensible framework for building custom interactive UI elements within the Lean 4 proof assistant.