Making Lean web games

Stream: Lean for teaching

[Kevin Buzzard]

I just put up a skeleton repo

https://github.com/kbuzzard/lean-game-skeleton

for use with @Mohammad Pedramfar 's Lean game maker. I might try and knock up a basic real number game this weekend, because I think there will be a demand from Imperial's undergraduates (who will have a test on sup/inf and sequences/limits in January). Other things on my todo list:

(1) finish inequality world for the natural number game (this won't take long, but I'm happy with the current state of nng so I put it lower down the list)
(2) Add some more levels to natural number game (odd/even world, prime number world are two that spring to mind, although maybe one wants subtraction world and div/mod world first; this is even further down the list than (1))
(3) The Integer Game. Introduce Lean's concept of quotient to mathematicians by defining $\mathbb{Z}$ to be $\mathbb{N}^2/\sim$ with $(a,b)\sim(c,d)\iff a+d=b+c$. Go on to prove that the integers are a commutative ring. I have no real feeling as to how hard/interesting this will be. Whilst introducing quotients is probably a good thing (and in particular some thought will be needed about how to teach mathematicians how to use Lean's quotients) part of me feels like this is just "more of the same" -- checking that addition is well-defined on integers just amounts to a bunch more natural number game levels. So it's also low down the list.

I look at the above things and at the real number game and I can see a genuine need for the real number game now (to get 1st year maths students who are learning about sup and inf / limits of sequences now into Lean) so I think my efforts are better concentrated on the real number game. Making these games takes some time because you have never taught people enough things. e.g. I thought that proving basic things about sups would be easy but then I realised I needed to teach them basic things about sets first; I thought that proving basic things about limits would be easy but then I realised that users have no idea how to control stuff like max etc etc.