Chalkdust is a great magazine for undergraduates which circulates in hard copy form around London and is also available online. It’s quirky, it’s put together by people who know what they’re talking about, and I think it does a great job of promoting mathematics to the undergraduate and school communities in London and beyond. And issue 10, out today, has an article about Lean in it ðŸ˜€ [disclaimer: written by me ðŸ˜‰ ]

The reason this article got written was that I was at the launch party for the last issue, and got talking to Eleanor Doman, one of the people behind the magazine. She’d seen me give a school talk and asked if I had anything I wanted to contribute. Two years ago I had written a blog post about the natural numbers which had proved quite popular with Imperial’s undergraduates, on proving basic theorems about the natural numbers just from Peano’s axioms. People told me that it was a good gateway into learning how to use Lean. I decided it was worth revisiting this idea, and wrote the article linked to above. But I also thought it was about time I made this stuff easier for people to try themselves, and so, with many many thanks to Mohammad Pedramfar who did all the web coding, we present to you…

## The Natural Number Game!

Ever wanted to prove that and implies from first principles, but couldn’t be bothered to download and install a computer theorem prover? Well now you can! The natural number game is an atttempt by me to teach complete beginners, who are comfortable with induction but know nothing about theorem provers, how it feels to use one. Undergraduate mathematicians — this is a chance to try Lean without having to download anything, and get over enough of the learning curve to get going and actually do something without getting stuck 100 times. Or maybe you’ll get stuck 100 times anyway. Find me on the Lean chat and give me feedback.

Currently we have around 50 levels, covering addition, multiplication, raising numbers to powers, and a few inequality levels. Over the next few weeks I hope to add 20 more inequality levels and some stuff about even and odd numbers and primality.

If you’re not a fan of the web interface and just want to play the game offline on your own computer, you’ll need to install Lean and its maths library, but this is not too hard nowadays. The natural number game source code is available online at github with installation instructions.

This is great! Bug report, the variable names in the code and the normal math don’t match for World 3, Level 4.

LikeLiked by 1 person

Thanks! Happy to hear more. I’ve caught a couple of things myself. Will release v1.01 when I have a minute.

LikeLike

I’m not sure this is a bug or what. World 1, Level 4.

I type:

rw \l h, rw h, refl,

OK, nothing yet, other than it tells me the refl tactic is being used at 100:19.

But then I delete the last comma… Suddenly my proof is complete?

LikeLike

The truth about commas is that Lean *does not need the very last one in a complete proof* but I decided against emphasising this. So your proof is complete with or without the very last comma. Notice that the second rewrite actually changes two things not one ðŸ˜€

LikeLike

I played through the whole thing. Some comments/questions/observations.

I think it might be helpful to reveal “intended solutions”/”optimal solutions” after you succeed at a given level. I often forgot the syntax for some basic operation, tried several times to do it and failed, then gave up and solved the problem a different and wordier way. Seeing a curated solution would let me know if I was on the right track originally and teach me the correct syntax if so. The “pro-er tip” on world 5, level 2 is a great example of information I would want to see after solving the level rather than before.

Other times I didn’t know the syntax to do something, figured out a more cumbersome alternate approach, and only read the correct syntax in a hint to a much later level. The hints on World 5, level 2 and world 5, level 6 are both examples of this. Are we supposed to use these earlier? Was I trying completely the wrong way?

Is it possible to solve all the levels without using tactics that are not on the list you linked to? (In particular, the contradiction tactic)? I guess an intended solutions list would answer this as well.

I didn’t like the hints very much. I tried not to read them and to just look at the problem, and when I saw the hints I tried to solve the problems without following the hints (and usually failed). I wonder if some of them could be removed, or hidden in some optional hints box. Also the “start with intro h” hint on World 5, Level 4 seems wrong. I think you meant “start with cases h”.

LikeLiked by 1 person

The truth of it is that the game was rushed out before it was finished, because I wanted it to coincide with the Chalkdust article but I was really drowning in teaching. Thanks loads for the comments Will. I am going to release a better v1.1 hopefully soon. The answer to questions like “is it possible to solve all the levels without using tactics not on the list” is “I really have no idea, this is shoddy on my part I know”.

LikeLike

I observed several times that getting some bit of the syntax slightly wrong just resulted in the top right window going blank without any helpful error messages in the bottom right window.

I noticed that starting typing e.g. an apply tactic tended to make the top right window go blank while typing (just saying e.g. “85:7: tactic apply”). But it would be helpful to have the hypotheses and goals stay visible there to help in figuring out exactly what to put in the command I’m typing.

Particular places (in world 2, I haven’t gone further than that) where I knew what I wanted to do mathematically (but which might have been different from the intended proof approach!) but in doing so it seemed necessary to refer to external documentation, were where it started using “not equal” with more than just symmetry (I didn’t see any guidance on how to use, or prove, propositions involving “not”, though some guesswork found it worked as “implies false” for “intro”, or how to dispose of a case once you’ve successfully derived a contradiction such as x \ne x or a = succ a), and where I wanted to apply theorems given in an “iff” form and so ended up looking up iff.elim_left to convert them to an “implies” form.

World 2, Level 6 has a typo “numebrs”. (I could file a pull request for that fix if you want, but I guess it’s quicker for you just to fix it.)

LikeLiked by 1 person

Hi Joseph! The poor error reporting is actually a bug in https://github.com/mpedramfar/Lean-game-maker which has since been fixed (but the fix hasn’t made it to the web version of the game yet). World 2 the higher levels are just all belched out with no thought about how to teach beginners how to do them, I’m sorry. This needs fixing but I’m very busy with work right now. I’m hoping to get something better out within a week.

LikeLike

Some more observations:

The tactic guide in the left column really ought to link to https://wwwf.imperial.ac.uk/~buzzard/xena/html/source/tactics/guide.html (and maybe to the Lean manuals) as the point where I find I want to look up more advanced tactics doesn’t tend to be from the particular levels that have that link.

Some of the lemmas / theorems are specified in a form like âˆ€ (a b : mynat) (and so to prove them I need to start with “intro” on those variables), others just use (a b : mynat); I’m not sure if this difference is accidental, deliberate to introduce different language features, or deliberate because there is some reason it’s idiomatic to use âˆ€ in certain cases but not others. Yet others use {a b : mynat}, meaning that to specify arguments explicitly when using them it’s necessary to discover the “@theorem_name” syntax for specifying such arguments in the {} case. It would be least confusing for this beginner just to use (a b : mynat) all the time.

LikeLiked by 1 person

Joseph it’s all accidental. Thank you very much for your careful comments. I used to have a lot of { }s and then at the last minute I attempted to change them all to ( )’s but clearly I missed a few. It got rushed out the door. I only now have the time to look at it carefully.

LikeLiked by 1 person

And having now done all the levels: World 5, Level 1 clearly has problems with the formatting (mostly just showing raw source of the level rather than formatted like the other levels). In World 5, the left column of known results ought to include le_def rather than starting with le_refl.

Thanks for putting this together! Looking forward to additional Worlds and Levels in future.

LikeLike

Joseph thanks for playing it all the way through before I myself had got around to this ðŸ˜€ I only added world 5 a couple of days before release. I have 30 results about inequalities which need to go in there. I then have to decide whether to do more stuff on naturals (even/oddness, primality, maybe even uniqueness of factorization) or whether to start on The Integer Game!

LikeLike

OK I think that all the issues raised here are fixed in the current version of the game.

LikeLike