My comments on Natural number game

Stream: new members

[Ville Salo]

I wrote up my comments and complaints about the Natural number game as I went https://pastebin.com/pvvBmBnT in case someone is interested; I imagine this is useful data, but if it's not, feel free to ignore, cost me nothing to write it down. (I am a relative noob, I finished the game in maybe 4 hours. Maybe a year ago I spent a few days reading about Lean, and I do have some past functional programming experience.)

[Kevin Buzzard]

Nice job! Install lean on your computer following the instructions at https://leanprover-community.github.io/get_started.html and then clone the repo with leanproject get ImperialCollegeLondon/natural_number_game, open the root directory of the project in VS Code and then navigate to src/game/world10/level18q.lean and see if you can prove strong induction :-)

Re: your comments. (1) yeah people do stuff in different ways to the official solutions (available here) and it is somehow impossible to explain all the relevant tactics for all approaches. (2) yeah there's nothing I can do about 0; defaulting to nat is baked into core Lean 3 (3) yes it's exactly all about the brackets. () means "you need to write this", {} means "Lean's elaborator will figure it out". (4) yeah, sorry, it's a bit clunky. This is because you're running an interactive theorem prover in javascript. (5) yeah, in VS Code there are tools like "pause".