A Lean-based language for teaching proof in high school

DOI10.1007/978-3-032-07021-0_25MaRDI QIDQ6856393zbMATH OpenFDO

Authors Frédéric Tran Minh, Laure Gonnord, Julien Narboux

Publication date 19 February 2026

Full work available at URL https://doi.org/10.1007/978-3-032-07021-0_25

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Cites work

• A vernacular for coherent logic
• An extensible user interface for Lean 4
• Automated Deduction – CADE-20
• Congruence closure in intensional type theory
• First order logic with domain conditions
• scientific article; zbMATH DE number 2154400 (Why is no real title available?)
• Reconstructing proofs at the assertion level
• Teaching mathematics using Lean and controlled natural language

This page was built for publication: A Lean-based language for teaching proof in high school

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