logo for basementcommunity

basement
community

search

wall of shame

video games Natural Number Game

joined feb 22, 2023

avatar

Do not induce vomiting if swallowed.

joined feb 22, 2023

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.

posted 1/19/2024, 12:18 am

joined dec 5, 2022

avatar

testing one two

joined dec 5, 2022

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.

posted 1/21/2024, 8:09 pm

joined dec 5, 2022

avatar

testing one two

joined dec 5, 2022

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

posted 1/22/2024, 12:27 pm

joined dec 5, 2022

avatar

testing one two

joined dec 5, 2022

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.

posted 1/29/2024, 4:41 pm

joined feb 22, 2023

avatar

Do not induce vomiting if swallowed.

joined feb 22, 2023

quoting thatbirdguy:

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

posted 1/30/2024, 2:07 am

video games Natural Number Game