FAQ.

Contents:
  • The game doesn't work :-(
  • My proof doesn't work :-(
  • My proof which shouldn't work, works!
  • I finished the game. What do I do now?
  • How come real Lean is a bit different to this?
  • Will there be any more of this game?
  • Will there be any other games like this?
  • Where is the source code to this game, and how did you make it?

    • The game doesn't work :-(

    This game needs cookies to work, so it will not work in e.g. private browsing or incognito mode. The reason it needs cookies is that it downloads a javascript version of an entire computer proof verification system onto your computer. Some browsers sometime have issues. Last time I checked the game worked fine in Chrome and Firefox. It usually works in other browsers too. If you see "Lean is busy" and it hasn't gone away after about 20 seconds, it's not working -- try another browser or try enabling cookies. There was a problem with Safari 13.0.3, but Safari 13.1 apparently works fine.

    My proof doesn't work :-(

    This is hard to diagnose. There are two problems: syntax errors (where you missed a comma, or typed "induction wit" instead of "induction with"), and errors with your Lean code (a rewrite failing). For syntax errors: look at the first error in the bottom right hand box. It will probably have a red "33:2 error:" warning above it. That is the line number, and the character number on that line, of the first error. The character there is your problem. For errors in your Lean code, well, Lean is very picky. You might have to ask at the Zulip Lean chat.

    My proof which shouldn't work, works!

    The refl tactic is more powerful than you think. refl will close a goal of the form X = Y if X and Y are definitionally equal. For example, n + 0 is defined to be n, so the goal n + 0 = n can actually be proved by refl. However 0 + n = n is only true because of a theorem (proved by induction), so you cannot close this goal with refl.

    I finished the game, what do I do now?

    You can try the Lean maths challenges on CoCalc or using the Lean web editor . These are undergraduate level mathemamatics challenges involving equivalence relations, group theory and so on. To go further you should install Lean on your own computer and then create a project of your own, or download the tutorial project. The tutorial project contains, for example, a step-by-step guide to proving the intermediate value theorem in Lean. I (Kevin Buzzard) teach an undergraduate maths course to 1st years at Imperial, and I have been formalising the example sheets. You can try these if you know undergraduate level mathematics. At the time of writing there are still around 30 perfectoid space levels . You'll need to know a whole bunch of Lean and also a whole bunch of commutative algebra to do these. Once we've done all of them, we will get a formally verified example of a non-empty perfectoid space. This is a research project.

    More of my hopes and dreams are listed here . This list gets added to far more often than things are removed from it. That is the nature of the game at this point in time. Things will change.

    Finally, there are often problems kicking around on the Zulip Lean chat . Login required, real names preferred, be nice.

    How come real Lean is different to this?

    If you want more efficient Lean experience, e.g. you want to go beyond the natural number game and do more mathematics in Lean, then you can install Lean on your own computer and then create a project of your own, or download the tutorial project. If you do this, then you might notice that real Lean is slightly different. For example, the rw tactic in real Lean actually tries refl afterwards, so some goals get closed quicker than you think. I disabled this in the natural number game because I felt it was confusing for beginners. Other tactics I beefed up a little -- for example the induction and cases tactics in real Lean might leave you with goals mentioning mynat.zero, and in natural number game Lean these automatically get converted to 0. The meta code which enabled me to do this was written by Rob Lewis and you can take a look at how he did it here.

    Will there be any more of this game?

    There are a few more levels which I haven't added yet; they will come in v1.4, which will be the next version of this game. It is basically 15 or so more levels about less-than, which will culminate in a proof that the natural numbers are an ordered semiring, and strong induction works. Adding stuff about even and odd numbers should be easy, and one could even envisage developing a basic theory of primes and factorization in future versions. I want to concentrate on other games right now though.

    Will there be any more games like this?

    Hopefully. The integer game, the real number game, the group theory game are all ideas which are in various stages of completion as I write. The one in active development right now is the real number game.

    Where is the source code to this game, and how did you make it?

    The Lean source code is at this github repo, and the tool we used to turn it from Lean code to a browser game is the Lean Game Maker.