natural number game

Stream: general

[Oliver Fuchs]

3:49 PM

Hi, I am new in natural number game. I have to proof succ(a)b=ab+b but i cant. But i can proof add_mul by my own. With this I can proof succ(a)b=ab+b. How can I add add_mul as theorem to the multiplication world? thans.

[Mario Carneiro]

You should be able to use all proofs you have done in previous levels

[Mario Carneiro]

so once you have done add_mul you can use apply add_mul or rw add_mul or have := add_mul a b c to use the add_mul theorem

[Oliver Fuchs]

Thanks, I tried already to install Lean on my computer. There it must be possible to start my own natural number game.
But the import advises

import mynat.definition -- imports the natural numbers {0,1,2,3,4,...}.
import mynat.add -- imports definition of addition on the natural numbers.
import mynat.mul -- imports definition of multiplication on the natural numbers.
gave an error. How can I import these definitioins?

[Mario Carneiro]

I don't think NNG is intended for offline use, but I think it's possible if you download the NNG repo

[Kevin Buzzard]

You should install leanproject following the instructions on the community website and then use it to install the natural number game

[Gihan Marasingha]

I'm using the NNG platform to write some games but I find, for some reason, that adding locale/content.pot to .gitignore has no effect. Has anyone else had this issue?

Never mind. I figured out that I needed to do git rm --cached locale/content.pot first.

[Kevin Buzzard]

I'd love to set what you come up with! Things like the complex number game could probably be made into web apps via this. There's also a good filter game one could make

[Gihan Marasingha]

Oooh, I had been thinking about a filter game (I was inspired by your TCC course) and that's next on my list. At the moment, I'm doing an even more basic intro to Lean that the NNG, focussing on using rewrites to manipulate integer equations.

[Kevin Buzzard]

Interesting!

[Kevin Buzzard]

Let me know if you want beta testers (give James a URL and he can advertise it on the Discord)

[Gihan Marasingha]

Thanks. Will do!