DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2024.27

Teaching Mathematics Using Lean and Controlled Natural Language

Authors: Patrick Massot

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract

We present Verbose Lean, a library using the flexibility of the Lean programming language and proof assistant to teach undergrad mathematics students how to read and write traditional paper proofs. After explaining our main pedagogical goals, we explain how students use the library with varying levels of assistance to write proofs that are easy to transfer to paper because they look like natural language. We then describe how teachers can customize the student experience based on their specific pedagogical goals and constraints. Finally we describe some aspects of the implementation of the library, emphasizing how new aspects of the very recently released version 4 of Lean allow a lot of flexibility that could benefit many new creative uses of a proof assistant.

Cite as

Patrick Massot. Teaching Mathematics Using Lean and Controlled Natural Language. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 27:1-27:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{massot:LIPIcs.ITP.2024.27,
  author =	{Massot, Patrick},
  title =	{{Teaching Mathematics Using Lean and Controlled Natural Language}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{27:1--27:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.27},
  URN =		{urn:nbn:de:0030-drops-207550},
  doi =		{10.4230/LIPIcs.ITP.2024.27},
  annote =	{Keywords: mathematics teaching, proof assistant, controlled natural language}
}

Search Results

Documents authored by Massot, Patrick

Teaching Mathematics Using Lean and Controlled Natural Language

Abstract

Cite as

Thanks for your feedback!

Could not send message