So something stupid happened. I had decided “no Lean” for the algebraic geometry course I’m teaching this term, and then I went to Lean Together 2020 and ended up on the plane back trying to formalise Martin Orr’s notes in Lean and now I’m seriously thinking about going for it and seeing how much we can do. It’s the theory of varieties. At the minute we’re doing affine algebraic varieties over algebraically closed fields. I might back off later if it gets tough, but I am eyeing the Nullstellensatz. They’ve done it in Isabelle. So it could well be possible in Lean 3. Can we *state* the Nullstellensatz in Lean 4? I saw people using Lean 4 last week. You still have to know what you’re doing, and probably using emacs is your best bet, but it is usable.

You won’t be using Lean 4 unless you’re an expert in this stuff, but here’s a challenge for mathematicians: read this proof. It’s my Lean write-up of lecture 1. That Lean file is 184 lines long, and it proves that the union of two algebraic subsets of is also an algebraic subset of . If you are a mathematician — give it a go. I bet you understand the first half of it. Then it gets technical because a proof starts, but even if you can’t understand the Lean code, I am still explaining in the comments what is going on. I mentioned in my last post how Hales and Koepke are thinking hard about making it easier for human mathematicians to use this kind of software. Until then, you need Rosetta Stones, and this Lean file is an attempt to give one. If you have Lean installed on your computer, then you can clone the repository for the course, run the code on your own computer and see Lean’s tactic state at every point. This makes it much easier to figure out what is going on. It is not always easy. However, it is sometimes easy, especially if you have played the natural number game. Look — there’s `zero_mul`

on line 132. If you don’t know about `zero_mul`

then you could play the natural number game, or try some maths challenges for the Lean curious.

How come everything goes so well up until the proof? Well, notation is a nightmare. Can this be fixed in Lean 4? Why does the goal often look incomprehensible? Why do I have to write `mv_polynomial (fin n) k`

instead of ? Why do I see `fin n → k`

instead of ? Why I am I taking intersections over all of the proofs that ? That makes no sense to a mathematician. How can we make this better? It’s just a normal proof presented in a scary way — but I am sure that we can make it less scary with current technology. This is one of the things I hope to work on this term.