2026-08-10T11:21:31Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18399 2024-03-06T11:01:48Z ddc:004 open_access

An Extensible User Interface for Lean 4 Nawrocki, Wojciech Ayers, Edward W. Ebner, Gabriel user interfaces human-computer interaction Lean Contemporary proof assistants rely on complex automation and process libraries with millions of lines of code. At these scales, understanding the emergent interactions between components can be a serious challenge. One way of managing complexity, long established in informal practice, is through varying external representations. For instance, algebraic notation facilitates term-based reasoning whereas geometric diagrams invoke spatial intuition. Objects viewed one way become much simpler than when viewed differently. In contrast, modern general-purpose ITP systems usually only support limited, textual representations. Treating this as a problem of human-computer interaction, we aim to demonstrate that presentations - UI elements that store references to the objects they are displaying - are a fruitful way of thinking about ITP interface design. They allow us to make headway on two fronts - introspection of prover internals and support for diagrammatic reasoning. To this end we have built an extensible user interface for the Lean 4 prover with an associated ProofWidgets 4 library of presentation-based UI components. We demonstrate the system with several examples including type information popups, structured traces, contextual suggestions, a display for algebraic reasoning, and visualizations of red-black trees. Our interface is already part of the core Lean distribution. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Wojciech Nawrocki and Edward W. Ayers and Gabriel Ebner 2023 Is Part Of LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2023.24 urn:nbn:de:0030-drops-183991 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.24 eng https://creativecommons.org/licenses/by/4.0/legalcode