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 ![k[X_1,X_2,\ldots,X_n]](https://s0.wp.com/latex.php?latex=k%5BX_1%2CX_2%2C%5Cldots%2CX_n%5D&bg=ffffff&fg=333333&s=0&c=20201002)
? 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.
Like this:
Like Loading...
Related
About xenaproject
The Xena Project aims to get mathematics undergraduates (at Imperial College and beyond) trained in the art of formalising mathematics on a computer. Why? Because I have this feeling that digitising mathematics will be really important one day.
Xena 
Why ARE you “taking intersections over all the proofs that
“? That sounds completely bananas.
LikeLike
It is absolutely bananas, and the answer is that I had misunderstood which functions to use when manipulating unions. There are three kinds of unions in Lean — union over a set of sets, union over a family of sets indexed by some type (so now we can have repeats) and union over a family of sets indexed by a subset of a type. All of these three things come up in “real world” mathematics and mathematicians don’t usually worry too much about distinguishing between them. When formalising you have to be clear about which ones you’re using and then use the appropriate functions designed to manipulate them. I was using the wrong ones.
LikeLike
There are also ways to fix the notation, which I learnt about on the Lean chat, so things are much better now. But they’re still not perfect — one can only go so far. For example the usual character n and the superscript n and the subscript n are three different characters and hence three different tokens, so there is only so much you can do. I’m pretty sure that unicode doesn’t have superscripts for every mathematical symbol, so maybe even $k^{a+b}$ will be hard to even type. We muddle on. Mathematicians who want to learn the software need to learn new notations for things currently 😦 But the intersection over proofs is gone 😀
LikeLike