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.