An extensible user interface for Lean 4

DOI10.4230/LIPICS.ITP.2023.24MaRDI QIDQ6643006zbMATH OpenFDO

Authors Wojciech Nawrocki, Gabriel Ebner

Publication date 26 November 2024

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2023.24

zbMATH Keywords

human-computer interactionLeanuser interfaces

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cited in

(6)

• Incorporating a database of graphs into a proof assistant
• A Lean-based language for teaching proof in high school
• Exploring formal math on the blockchain: an explorer for Proofgold
• Graphical rewriting for diagrammatic reasoning in monoidal categories in Lean4 (short paper)
• Teaching mathematics using Lean and controlled natural language
• Automated reasoning for mathematics

This page was built for publication: An extensible user interface for Lean 4

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6643006)