skip to content

Department of Computer Science and Technology

Thursday, 16 May, 2024 - 17:00 to 18:00
Patrick Massot (Université Paris-Saclay and Carnegie Mellon University)
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 : Meeting ID: 370 771 279 261 Passcode: iCo7a5

Seminar series: 
Formalisation of mathematics with interactive theorem provers

Upcoming seminars