Seminar Details
ProofWidgets4 - Diagram and Reference in Lean
- Start Date: November 29, 2023
- Event Start Time: 1:00 PM
- Event End Time: 2:00 PM
- Seminar Series: Rutgers LEAN (Mathematics) Seminar
- Presenter(s): Wojciech Nawrocki - Carnegie Mellon University
- Event Location: Hill Center, Room 525 and Zoom
- Event Additional Info: <p>This seminar can be attended either in person in Hill 525 or on line on<br /> Zoom: <a href="https://rutgers.zoom.us/j/94535910358?pwd=Y1UzREoxaDA2dUExek00Vm45TzE3dz09">https://rutgers.zoom.us/j/94535910358?pwd=Y1UzREoxaDA2dUExek00Vm45TzE3dz09</a></p>
- Presentation Type: Stand Alone Presentation
- Abstract:
When developing mathematics collaboratively on a blackboard, it is easy and natural to draw things and to refer to them: "Which polynomial?" "This one!" (said while pointing at, or otherwise indicating, the object of interest).
Development environments for most programming languages are not like this. They are generally text-based and non-referential: for instance when the checker produces a typing error, there is no way to learn more about the types contained therein because all contextual information has been thrown away by the time the error shows up on-display. The situation in formal mathematics is varied, but not uniformly better.
I will discuss the design of ProofWidgets4, a library of user interface components for the Lean theorem prover.
I will show in practice how ProofWidgets4 enables extending the editor environment with visual, referential components for diagrammatic mathematics, and for introspection of Lean's internals. Upcoming ease-of-life features may also be discussed.
(ProofWidgets4 (https://github.com/leanprover-community/ProofWidgets4))