From Informal to Formal and Back - Teaching Mathematics with Lean and Natural Language

Explore the bridge between formal and informal mathematical proof systems in this lecture that examines two innovative approaches to mathematical education and communication. Learn about Verbose Lean, a teaching library designed to help students transition from computer-assisted proofs to traditional paper proofs using controlled natural language and custom automation within the Lean theorem prover. Discover how this approach prioritizes skill transfer over coding ease, sharing methodologies with the Rocq Waterproof library. Examine the Informal Lean project, a collaborative effort to transform Lean proof files into interactive web pages presented in natural language, allowing readers to customize their level of mathematical detail and engagement with formal proofs.