## Stream: new members

### Topic: next step after nonnegative integer game

#### Darij Grinberg (Jan 04 2021 at 18:41):

so I'm wondering, what's the obvious next step after the nonnegative integer game?

#### Darij Grinberg (Jan 04 2021 at 18:42):

ideally i'd want to formalize some combinatorics or constructive algebra

#### Kevin Buzzard (Jan 04 2021 at 18:42):

@Bhavik Mehta formalised a bunch of combinatorics (Cambridge Part III level, like Kruskal Katona theorem)

aha

#### Darij Grinberg (Jan 04 2021 at 18:43):

it's part of mathlib?

#### Kevin Buzzard (Jan 04 2021 at 18:43):

I think that you would be best off just choosing a topic and announcing that you're going to work on that and then just starting. This worked really well for me

#### Kevin Buzzard (Jan 04 2021 at 18:44):

https://b-mehta.github.io/combinatorics/

#### Bhavik Mehta (Jan 04 2021 at 18:44):

Darij Grinberg said:

it's part of mathlib?

Not yet, there's some open PRs though

#### Darij Grinberg (Jan 04 2021 at 18:46):

aha. i assume using any packages like this requires a local install (as opposed to the web editor)?

#### Kevin Buzzard (Jan 04 2021 at 18:56):

Yes, this would make your life much easier. Instructions here.

(deleted)

#### Julian Berman (Jan 04 2021 at 19:02):

Kevin Buzzard said:

https://b-mehta.github.io/combinatorics/

Oh wow this page is great, don't think I've seen this yet myself.

thank you!

#### Bhavik Mehta (Jan 04 2021 at 19:50):

Julian Berman said:

Kevin Buzzard said:

https://b-mehta.github.io/combinatorics/

Oh wow this page is great, don't think I've seen this yet myself.

It's very old! I think it was before leanproject was even a thing (or maybe just before I understood how to use it)

#### Julian Berman (Jan 04 2021 at 21:25):

@Bhavik Mehta still, I haven't the vaguest idea what a perfectoid space is but I at least know what Kruskal-Katona is :D so reading that will be fun.

Last updated: May 18 2021 at 15:14 UTC