Can you import the definitions and theorems covered in NNG?

Stream: new members

[Samuel Webb]

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]

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

[Samuel Webb]

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]

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]

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]

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

[Kevin Buzzard]

Just clone the repo and build on it?

[Jireh Loreaux]

(deleted)