next step after nonnegative integer game

Stream: new members

[Darij Grinberg]

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

[Darij Grinberg]

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

[Kevin Buzzard]

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

[Darij Grinberg]

aha

[Darij Grinberg]

it's part of mathlib?

[Kevin Buzzard]

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]

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

[Bhavik Mehta]

Darij Grinberg said:

it's part of mathlib?

Not yet, there's some open PRs though

[Darij Grinberg]

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

[Kevin Buzzard]

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

[Aaron Anderson]

(deleted)

[Julian Berman]

Kevin Buzzard said:

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

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

[Darij Grinberg]

thank you!

[Bhavik Mehta]

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]

@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.

[Yaël Dillies]

@Darij Grinberg said:

it's part of mathlib?

Update: It's mostly part of mathlib now! We're still missing the titular Kruskal-Katona and Erdös-Ko-Rado, but the rest is in.

[Darij Grinberg]

thank you!