adam.math.hhu.de

I was referred this recently, and it's become an unhealthy addiction. Teaches basics of the Lean theorem prover, through building the theory of natural numbers from scratch. Once you've finished, there's also the set theory game (which I'm currently working through), and a couple others if you happen to speak German or Spanish.

phew I just completed the tutorial world! This is really addictive and also a great way to learn about logic. Can't wait to tacle Fermat's last theorem.

And just completed Addition World. I am not sure how I did it - I think I'll redo and take notes along the way.

I think I've run into a wall here, maybe you can give me a pointer:

I'm at level 2 of ≤ World where I am to prove: "If xx is a number, then 0≤x0≤x" and the tip suggests I perform the Use command with a number, C, to get started.

But when I try following the tool-tip I'm told that my number C is an unknown identifier, which I suppose it correct since it's not been introduced or anything.

Try using use on the variable you do have