Hello everyone! It has been quite a while since I have written anything here—my last post was in March 2020, and since then I have been overwhelmed dealing with online and hybrid teaching, plus a newborn (who is now almost 5 months old and very cute):
But the spring semester is finally over, and I have a sabbatical in the fall, so I plan to do a bunch more writing! I have several ideas of things to come (feel free to send me suggestions as well), but to start things out for today I just have a fun link:
The idea is to use a computer proof assistant to formally prove a lot of basic facts about arithmetic. That is, you get to build proofs using a special precise notation, and the computer will automatically check whether your proof is correct. But the whole thing is organized like a game, with a tutorial, levels that build on each other and introduce new ideas and techniques just before you need them, etc. It’s a lot of fun and honestly kind of addicting.
There is very little background needed other than some capability for abstract thinking. Things start out quite easy and progress slowly, though things become quite challenging by the time you make it all the way to the end.
The Math Less Traveled 
Here is one of my favorite playgrounds ☞ Riffs & Rotes
Very cool, thanks for sharing. I will have to study that, I don’t immediately see why we don’t just get all binary trees as possible shapes of drfs.
Congratulations on the newborn, and my sympathy for going through this last year as a teacher.
Thank you!
For Advanced Addition world Level 1, I get the impression that this two-line solution is not supposed to work, since it doesn’t make use of succ_inj:
cases hs with h1 h2,
refl,
Did I break their game?
Good find! You didn’t break it. In fact, what you have shown is that injectivity of constructors like succ is actually inherently built into the system. The text calls succ_inj an “axiom” but actually succ_inj can itself be proved using more fundamental constructs (think of the existence of the “cases” tactic as the real “axiom”.) In fact if you look at the source code for the natural numbers game here, you can see how succ_inj is defined:
https://github.com/ImperialCollegeLondon/natural_number_game/blob/master/src/mynat/definition.lean#L34
The definition looks… familiar. =) That is, instead of using succ_inj itself, you just used its definition directly.