The complex number game

Mohammad and I spruced up the natural number game over the last few weeks. It now saves your progress, which is great (thanks Mohammad). Also coming along nicely is the real number game, currently written mostly by Dan Stanescu, but Gavin Thomson has just joined the party and I promise that I will be contributing in June when marking is over. Anyone who wants to get sneak previews of it should hang around on the Xena Discord server, which is where our Thursday evening Xena Project meetings are taking place this term; I’ll probably release a secret alpha this coming Thursday. Last Thursday on the Discord we had people any% speedrunning and racing the Lean tutorial project . This fits very well into my general worldview: I think that doing mathematics in Lean is like solving levels in a computer puzzle game, the exciting thing being that mathematics is so rich that there are many many kinds of puzzles which you can solve. Level creators are conjecture makers. If you are into puzzle games and know a little Lean then you might also want to check out the Codewars website, where support for Lean just moved from beta to official; right now there are over 50 approved Lean Kata, ranging from easy facts about odd and even numbers to some very tricky Diophantine equations.

Another project I’ve been involved in is the forthcoming book Mathematics in Lean. Again I am guilty of doing very little so far. What I’ve been trying to do is to formalise “random” basic undergraduate mathematics in Lean as best I can, using as much automation as I can, in order to see whether it is possible to write basic tactic proofs in “the way a mathematician would write them”, but none of this stuff has made it into the book yet. It is miserable when when you are trying to prove a theorem in Lean and you’ve reduced it to a statement which is completely mathematically obvious (e.g. the goal is to prove that two things are “the same”), but you can’t persuade Lean to believe this, so the art is to set things up in such a way that this issue doesn’t occur, and one way of doing this is by seeking advice from people who understand type theory better than I do.

So I’ve been doing several experiments, hoping that some of them will turn from ideas into chapters of this book, and one which I think went quite well was a construction of the basic properties of the complex numbers, which I liked so much that I’ve put into its own repo for now: The Complex Number Game.

This repo came about with me looking at the official mathlib file for the complex numbers, and “remixing” it, re-ordering it so that it was a bit more coherent, removing some of the more obscure computer-sciency lemmas, and heading straight for the proof that the complexes are a ring. My rewrite of the mathlib proof is heavily documented and the proofs of all the lemmas along the way are in tactic mode; in my view this makes things more accessible to mathematicians. The file data.complex.basic in Lean’s library has been examined and revisited so many times since 2017 that it is now in very good shape — in particular lemmas are correctly tagged with simp and this makes simp a very powerful tool.

If you want to play the complex number game right now, you have to install Lean first. I would love to share this game on CoCalc but right now I can’t get imports to work. I will come back to this in June.

If installing Lean really is not something you want to do, then you can play a crappier preliminary version using the Lean Web Editor (this is before I reorganised the material to make it more mathematician-friendly and turned more proofs from term mode to tactic mode). Or you can just watch me play it! I live streamed on Twitch a walkthrough of the tutorial level (the complexes are a commutative ring) last Thursday, and here is the video. This Thursday (28th May 2020) at 5pm UK time (1600 UTC) I’ll be on Twitch again, live streaming a walkthrough of the first two levels: sqrt(-1), and complex conjugation. I’ll be on Twitch for around an hour, and then we will retire to Discord for a Q&A and more any% racing. Mathematicians who are Lean beginners are welcome!

Someone else doing some remixing is my daughter Kezia Xena Buzzard (after whom the project is named). She made my new profile pic from Chris Hughes’ proof of quadratic reciprocity 🙂

Advertisement