University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > Teaching using a proof assistant and controlled natural language

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹ️ Information

Teaching using a proof assistant and controlled natural language

Download to your calendar using vCal

If you have a question about this talk, please contact Anand Rao Tadipatri .

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

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Audit Room, King’s College, Cambridge Average on weekdays: 9041.24407583 kWh LR2, Dept of Engineering

Other talks

Shape modes of CP^1 vortices Fun experiments you can only do with frogs Chemical strategies for biomolecule functionalisation, and biomaterial conjugation Title to be confirmed Group Work Cambridge RNA Club - ONLINE
 

© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity