BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Teaching using a proof assistant and controlled natural language -
  Professor Patrick Massot (Université Paris-Saclay and Carnegie Mellon Un
 iversity)
DTSTART:20240516T160000Z
DTEND:20240516T170000Z
UID:TALK215755@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:I will report on the way I use Lean to teach first year math u
 ndergrads in Orsay. The main unusual thing is the use of a controlled natu
 ral language input syntax designed to make it easier to transfer proving s
 kills from the computer to paper. This will also be the opportunity to tak
 e a brief look at what meta-programming in Lean looks like\, and maybe ins
 pire you to build new things using this framework.\n\n—-\n\nWATCH ONLINE
  HERE : https://www.microsoft.com/en-gb/microsoft-teams/join-a-meeting?rtc
 =1 Meeting ID: 370 771 279 261 Passcode: iCo7a5\n\n
LOCATION:Live-streamed at MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR