Formalising number theory and geometry. A TCC course, Oct-Dec 2022.
Coordinates
Mondays 1600-1800, Teams. (no option for live lectures apparently -- I was misinformed -- I'll be giving them live from my office). Starts Monday 10th Oct 2022, and continues on Mondays. Four lectures, and then no lecture 7th November (I'm away), and then four more lectures. Last lecture 5th December 2022.
Registering
If you're at Bath, Bristol, Imperial, Oxford, Warwick or possibly Swansea then you can
register for the course; instructions are on the TCC website.
The course
Overview
This is a course about learning to write mathematical proofs on a computer. We will
be using a computer proof checker called Lean,
free open source software written by Microsoft Research which runs on all major operating systems. We will be using Lean 3
and its maths library mathlib. Lean turns a proof into a dynamic document, rather like Bret Victor's explorable explanations
but in the technical domain of pure mathematics. The idea of turning a proof into a dynamic document has potential for use in teaching, outreach and research in mathematics, although these things will not be explored in the course.
The course is in two four-week parts. The first four weeks we will spend doing basic stuff, learning how the system works. I will be getting you to do some of the work yourself. This part of the course is suitable for beginners who have not used Lean before. Then there's a week break because I'll be in Germany, and then there are four more weeks where I will be extending the algebraic geometry part of Lean's mathematics library, so we'll be doing basic "Hartshorne chapter 2" level stuff (basic properties of schemes and morphisms of schemes).
Prerequisites
The course will use Lean 3. You should install Lean and its mathematics library by carefully following the instructions here. There are no mathematical prerequisites for the first half of the course. For the second half I will assume that you know the basics of schemes. If you have no idea what Lean is, I would recommend taking a look at the natural number game. If you like it, and are interested in seeing more pure mathematics being done in this way, you might like the course.
Grades
If you need a grade for this course then your task is to write a project of your own, in Lean, on
some mathematics which interests you and which is relevant to the course (so ideally algebraic geometry).
Methodology
In the first half of the course we will be learning by doing. I will do some examples and then you do some examples and ask questions if you're stuck. In the second half I will do more of the work myself, but you can feel free to contribute too. We are teaching algebraic geometry to a computer and I'm pretty sure that we're not going to make it through all of the Stacks Project in four weeks.
The lectures:
Week 1: introduction to the subject matter, types and terms, some basic tactics.
Week 2: more basic tactics. First year analysis.
Homework
Week 1: get Lean installed and also install my formalising mathematics 2022 course. Course notes at .