Teaching Introduction to Proofs with Lean
Date: Wed, January 11, 2023
Room: Turing 0.E420
In Fall 2022, I taught an undergraduate course at Johns Hopkins University entitled “Introduction to Proofs” using the Lean Proof Assistant. In this talk, I will report on this teaching experiment.
Bohdan Liesnikov | Syntactical extensibility of proof assistants
Next: Jurgen Vinju | To parse or to marshall, that is the question