Zulip Chat Archive

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)

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

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.

Aaron Anderson (Jan 04 2021 at 19:01):

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

Darij Grinberg (Jan 04 2021 at 19:07):

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.

Yaël Dillies (Aug 06 2022 at 18:13):

@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 (Aug 06 2022 at 18:51):

thank you!


Last updated: Dec 20 2023 at 11:08 UTC