I just pushed an update to the natural number game. I’m rather pleased with how this has all worked out. I started off thinking it was kind of a game, but the explanations turned out so wordy and now I think it is kind of a book/game hybrid. I attempt to teach around ten key tactics: refl, rw, induction, intro, have, apply, exact, split, cases, left, right, exfalso. These are somehow the bare minimum that you can get away with. Many of the applications are mathematical rather than abstract logic stuff, so hopefully they are appealing to mathematicians.
To come: ≤ world. This will have a ton of levels, some quite tricky. Then I might do something about even/odd numbers, and possibly something about prime numbers if I have the time/energy.
And then what? I think there is potential for an integer game, and also for a basic analysis game with sups and infs and stuff, where the real numbers are presented as a black box complete archimedean field. In these games I would refer the player to the natural number game for tactic-learning and just get on with the levels. I have had a lot of positive feedback about the natural number game.
On the other hand, people have started asking questions such as “so what maths is in Lean exactly, nowadays?” and I don’t feel that there is a good answer to this on the internet at the minute — a half-baked answer I gave about 18 months ago when I was just getting on top of Lean is now woefully out of date. We even seem to have manifolds now, thanks to the heroic efforts of Sébastien Gouëzel. I think an equally important question is “what maths isn’t in Lean yet, but could be in it soon?” I will attempt to answer both of these questions in the near future. [update a few weeks later — see “what maths is in Lean” link above!]
Xena 
This is a lot smoother and better at explaining the required tactics than the original version, but I found a few more issues in the course of playing it anyway. Looking forward to seeing the answers to the questions you mention. (I think there’s another related group of questions of interest as well, but maybe harder to answer, “what would mathematicians working in branch X of maths like to see in Lean to be able to formalise their work?”.)
Addition world, Level 1 has typo “natual”.
Addition world level 6 says ten more levels about addition, but Advanced Addition world has 13 levels.
Multiplication world level 5 hint refers to “exact”, but “exact” hasn’t been introduced yet.
Multiplication world level 7 refers to “the end of world 4”, but worlds no longer have numbers.
At the bottom of Function world level 2, and again at the bottom of Advanced Proposition world level 9, there are “todo” notes that probably shouldn’t be visible to someone playing the game.
Some tactics, after being taught, don’t appear in the tactic guide on the left. This applies to at least “cc”, “by_cases”, “tauto”, “exfalso”, “revert”.
Advanced Addition world, level 5 refers to a proof ending “exact add_right_cancel”, but for me it only worked with “exact add_right_cancel _ _ _” which is taught in the following level.
The heading on Advanced Multiplication world level 4 says Multiplication World without Advanced.
At one point I got the game stuck in a “Lean is busy” state (after giving a bad “repeat” tactic instruction) and it wasn’t clear how to interrupt it.
LikeLike
I like the way you have managed to wipe your brain and start the game again 😀 Thanks Joseph!
LikeLike
It’s possible some levels were easier because I’d done them before and you need a fresh set of beginners to say whether this version is explaining everything adequately! 🙂
I sort of wonder if a more interesting next step after proving stuff about natural numbers isn’t “prove more stuff” (about other kinds of numbers) but “define stuff” (types, functions, theorem statements, etc.). But I don’t know how you could make a game out of the process of learning to write good definitions (as opposed to definitions that make sense to mathematicians but are bad for theorem provers).
LikeLike
Defining stuff is definitely the next step towards learning how to be a competent Lean user. But defining stuff and then setting up a framework so that proving things about the stuff you defined is not painful, is harder than a naive mathematician might think. I defined the complex numbers in Lean and then you have to get to the point where proving a*(b+c)=ab+ac is “check real and imaginary parts; done” but this involves training a tactic so that it knows how to handle your new objects.
The other reason I’m focussing on theorems is that I think they’re more fun.
LikeLike
Hi! In the Function world, Level 9, it says: “In world 6 we will see a variant…”, only the worlds are no longer numbered.
Best wishes!
LikeLike
Another one: in advanced addition world, level 5, “The theorem add_right_cancel is the theorem that you can cancel on the left” should say “cancel on the right”.
LikeLike
Another one (and you can delete these comments if you wish!): in the advanced addition world, level 10, near the start of the page it reads “cases b with b : mynat” instead of “cases b with d : mynat”
LikeLike
Thanks for all of these. Some are already fixed in the version on my laptop but I just need to find the time to push the new version to the website!
LikeLike
Hi!
I am working on the (new?) Inequalities world, and noticed that add_le_add_right and add_le_add_left have significantly different types; is this intentional?
LikeLike
That’s a really interesting comment, because I think that they have almost the same types 😉 Is the issue that I just moved the colon? The colon is somehow not part of the type.
LikeLike
As a computer science major with prior experience in Coq, I personally found the natural number game to be an excellent introduction to theorem proving in Lean, and recommending it to my programmer friends with no prior experience in theorem proving suggested that it was much easier to follow than other well-known introductory material on theorem-proving such as [Software Foundations](https://softwarefoundations.cis.upenn.edu), for those who do not already have a solid background in discrete mathematics.
However, one of my programmer friends going through the game recently got stuck on Level 4 of Advanced Multiplication World (proof of `mul_left_cancel`), and after a bit of discussion with him/her to figure out why he/she got stuck on that particular level, I would like to propose a possible improvement to the description of that level.
Even though the `revert` tactic is mentioned in that level as a “convenient tactic” to try, there is insufficient explanation as to what it means from a logical perspective and why using it would make the induction “go through” which otherwise wouldn’t (provided that the correct induction was chosen in the first place). In my humble opinion, the level would be more educational if the description were to be modified as follows: 1) instruct the solver to choose a particular (correct) induction after he/she `intros` everything, and observe how he/she gets stuck in the inductive case with the induction hypothesis not being applicable to the current goal; 2) ask the solver to try again with the same induction but with `revert b` before actually performing the induction, and observe how the induction hypothesis has changed (and how it has become applicable in the inductive case this time round). Finally, 3) explain the concept behind using `revert`, i.e. how leaving suitable variables quantified in the goal often gives a stronger induction hypothesis which is sometimes needed in induction proofs. Perhaps adding a few extra levels on this particular topic of strengthening the induction hypothesis would also be beneficial.
P.S. looking forward to your real number game 😉
LikeLike
Thanks for this. I am bogged down with teaching right now but I have every intention of coming back to the natural number game, tidying it up, getting it out of beta, and dealing with the many comments which people have sent me.
LikeLike
Small fix: the theorem list in Power World displays pow_succ (a b : mynat) :
a ^ succ(b) = a ^ b * b. I think that should be pow_succ (a b : mynat) :
a ^ succ(b) = a ^ b * a. It does behave correcly when used.
LikeLike
Ouch! Thanks!
LikeLike
Thanks for the work you’ve put into this! I really enjoyed the natural numbers game.
A minor comment: I really wish the game had introduced me to the “`specialize“` tactic. There were several points where I really wanted to use “`apply“` in a hypothesis, but of course “`apply“` only works for goals.
However, I understand that at no point do you actually need it, so I can appreciate not having introduced it for pedagogical reasons.
LikeLike
Thanks for this. I hardly ever use that tactic in real life. Can you get round it with using `have` or `replace`?
LikeLike
In the natural numbers game, there is certainly no need for it.
My guess is that, in general, you can always use `have` every time you wanted to use `specialize`, but I’ve found that at least sometimes,`specialize` can get you what you want with much less typing. (I find the syntax easier as well since I don’t need to remember where to put the `:` or `:=`.)
I’m not familiar with the `replace` tactic! Is that the same as `change`?
LikeLike
https://leanprover-community.github.io/mathlib_docs/tactics.html for all the tactics. Looks like `replace` is slightly more flexible.
LikeLike
I see. I had made the mistake of thinking all the tactics were listed on https://leanprover.github.io/theorem_proving_in_lean/tactics.html
Thanks for pointing that out!
LikeLike
I noticed the link at https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ is down. I was wondering if there is an alternative URL that works, or if there is a way to run this myself?
LikeLike
Chris Birkbeck is hosting a mirror at https://cbirkbeck.github.io/natural_number_game/
LikeLiked by 1 person
Sorry, it’s been really hit-and-miss recently; apparently there was some problem with the set-up which has since been resolved.
LikeLike