Zulip Chat Archive

Stream: new members

Topic: Can you import the definitions and theorems covered in NNG?

Samuel Webb (Nov 30 2023 at 17:22):

Is it possible to import the theorems and definitions from the natural number game to a separate project? If so would anyone be able to point me in the right direction of how?

Yaël Dillies (Nov 30 2023 at 17:24):

What theorems do you care about? Are the ones in Std enough?

Samuel Webb (Nov 30 2023 at 17:28):

I am hoping for all of the theorems in the natural number game at adam.math.hhu.de. Unfortunately I am not sure what you mean by Std.

Jireh Loreaux (Nov 30 2023 at 17:33):

What's your goal in importing the theorems? I'm not saying it's necessarily a bad idea, but if we knew where you were headed we would be better able to advise you.

Samuel Webb (Nov 30 2023 at 17:36):

Excellent question. For a project at uni we are hoping to produce some materials for further learning of lean based on the introduction to proof course we took in our first year. Which you would begin having completed the natural number game. So having the theorems and proofs from the NNG would provide some consistency.

Samuel Webb (Nov 30 2023 at 17:36):

There is also an element of continuing to build on your own library of proofs.

Kevin Buzzard (Nov 30 2023 at 18:06):

Just clone the repo and build on it?

Jireh Loreaux (Dec 01 2023 at 00:51):


Last updated: Dec 20 2023 at 11:08 UTC