Date:
Thursday, 16 May, 2024 - 17:00 to 18:00
Speaker:
Patrick Massot (Université Paris-Saclay and Carnegie Mellon University)
Venue:
Live-streamed at MR14 Centre for Mathematical Sciences
I will report on the way I use Lean to teach first year math undergrads in Orsay. The main unusual thing is the use of a controlled natural language input syntax designed to make it easier to transfer proving skills from the computer to paper. This will also be the opportunity to take a brief look at what meta-programming in Lean looks like, and maybe inspire you to build new things using this framework.
—-
WATCH ONLINE HERE : https://www.microsoft.com/en-gb/microsoft-teams/join-a-meeting?rtc=1 Meeting ID: 370 771 279 261 Passcode: iCo7a5
Seminar series:
Formalisation of mathematics with interactive theorem provers
