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.