Interactive Theorem Proving in Education and Research
Timetable
24 July 2024 // University of Exeter // Online
All times are in British Standard Time (UTC+1)
| Time | Speaker | Event |
|---|---|---|
| 09:30 | Introductory Lean workshop: Lean via the Game Engine | |
| 10:30 | Coffee break / Registration | |
| 11:00 | Athina Thoma | Learning Lean: Exploring students’ perspectives and use of Lean |
| 11:30 | Patrick Massot | Teaching using a proof assistant and controlled natural language |
| 12:00 | Questions | |
| 12:15 | Kevin Buzzard | The state of the art in the formalisation of research-level mathematics |
| 12:45 | Heather Macbeth | A “calculation-heavy” introduction to proof, with support from Lean |
| 13:15 | Questions | |
| 13:30 | Lunch Student posters | |
| 14:15 | Jeremy Avigad | Teaching with Lean |
| 14:45 | Achim Brucker Diego Marmsoler | Introducing Isabelle to students with little maths or theoretical computer science background |
| 15:15 | Questions | |
| 15:30 | Workshop: Mathematics in Lean | |
| 17:00 | Close |
Abstracts
Jeremy Avigad. Teaching with Lean
Interactive proof assistants are powerful tools for teaching, providing students with information, correction, and feedback in real time. More importantly, they also increase students’ motivation and engagement, making classes more fun for students to take and for instructors to teach. In this talk, I will discuss my experiences using Lean to teach mathematics and computer science to undergraduate students at Carnegie Mellon, as well as similar efforts by others.
Achim Brucker and Diego Marmsoler. Introducing Isabelle to students with little maths or theoretical computer science background
In this talk, we provide a gentle introduction to Isabelle/HOL, focusing particularly on our approach to teaching it to students with limited backgrounds in computational logic, mathematical proofs, or theoretical computer science. Instead of emphasizing proofs initially, we begin with an executable subset of higher-order logic (HOL) to specify functions in a functional programming style. Rather than proving properties of these functions immediately, we explore and systematically test them using Isabelle’s code generator. This approach helps students grasp the basics of Isabelle and develop a deeper understanding of functional correctness, safety, and security properties of functional programs. Finally, we introduce students to mathematical proofs by utilizing proof automation tools, such as Sledgehammer, to prove the thoroughly tested properties.
We have employed this “top-down” approach to teach Isabelle to students in our otherwise application-focused BSc Computer Science program. This method has allowed us to successfully supervise several final-year projects using Isabelle each year and has inspired students to pursue PhDs in formal verification using Isabelle/HOL.
Kevin Buzzard. The state of the art in the formalisation of research-level mathematics
We give an overview of what has been happening recently with regards to formalising modern mathematics in Lean.
Heather Macbeth. A “calculation-heavy” introduction to proof, with support from Lean
I will report on my experience teaching with Lean in an early-undergraduate (1st and 2nd year students) mathematics course: an American intro-to-proof course with an emphasis on concrete numeric examples. The course is genuinely bilingual between English and Lean, with every proof carried out in parallel formally and informally. Substantial custom automation supports proof-writing at the same level of detail as is required of the students on paper, notably in calculational proofs of equalities, inequalities and (modular-arithmetic) congruences.
Patrick Massot. Teaching using a proof assistant and controlled natural language
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.
Athina Thoma. Learning Lean: Exploring students’ perspectives and use of Lean
In this talk, I will share results from a few educational studies: exploring the impact of Lean on mathematics undergraduates’ pen and paper proof writing; investigating further students’ perspectives on the use of Lean; and exploring aspects of students’ activity when proving statements in Lean. More specifically, the latter study explores students’ activity when proving statements in the Natural Number Game.
Lean via the Game Engine
The purpose of this practical workshop is to introduce you to the basic concepts of Lean via a user-friendly interface, the Lean 4 game engine/server. The Lean 4 server is an open source project, hosted at the Heinrich Heine University that permits the creation of game-style learning environments.
Lean games are particularly useful for beginners and students as they (1) take away the pain of installation, dealing with repositories and (2) present a friendly, scaffolded interface.
We’ll use the Natural Number Game, by Kevin Buzzard and Jon Eugster. The plan is to work through (at least) the first two ‘worlds’ of this game, the tutorial world and the addition world. In the addition world, you will prove basic results concerning addition of natural numbers, using Lean’s version of the Peano formalisation of natural number addition.
Caveat: the natural number game redefines some of Lean’s fundamental tactics, such as rewrite, for pedagogical purposes.
By the end of the session, you should be familiar with the aspects of the game interface including:
- The home page of a game: erasing/uploading/downloading data. Using rules to skip levels and results.
- The tactics/definitions/theorems sidebar
- Line-at-a-time proof entry including
- Viewing hints and error messages.
- Retrying lines.
- Understanding objects, assumptions, goals.
- Working with multiple goals.
- The editor interface.
You’ll learn the following general concepts regarding proof in Lean:
- How Lean represents a proof state (a point in a proof) via hypotheses and goals.
- How ‘tactics’ are used to transform the proof state. In particular:
- Using the rfl tactic to prove equations of the form $$x= x$$.
- Using the rewrite tactic to:
- transform the goal using an equational hypothesis or a theorem, replacing occurrences of the left side of the equation with the right side.
- transforming the goal in the other direction (replacing occurrences of the right side of the equation with the left side).
- transforming hypotheses
- Using the induction tactic to prove theorems concerning the natural numbers. Via this you’ll see how to deal with multiple goals. In this instance, they are the base case and the inductive step.
Mathematics in Lean
In this practical, we’ll move on to ‘real-life’ Lean via the Mathematics in Lean online book. To work through the exercises, you’ll first need a GitHub account and you should then proceed to the Mathematics in Lean GitHub repository.
We’ll run Mathematics in Lean via a GitHub ‘Codespace’. This is (something like) a virtual computer running an instance of Visual Studio Code: a popular source code editor.
Getting started with Codespaces: Once you access the above repository through your GitHub account, click on the green ‘<> Code’ button and choose the ‘Codespace’ tab. Then click ‘Create codespace on master’. It will take a few minutes for GitHub to create your new codespace and download and install Lean and its mathematical library, Mathlib.
Returning to a Codespace: You don’t need to create a new codespace each time you return to your work! From the main Mathematics in Lean repository, click the small downward-pointing triangle in the green ‘<> Code’ button. From the ‘Codespace’ tab, select a currently running codespace. It will have a funny name like ‘supreme custard zeba’.
Aims: You will learn about Lean/Mathlib’s automation tactics including linarith, simp and explore parts of Lean’s mathematical library, Mathlib.