Zulip Chat Archive

Stream: new members

Topic: next step after nonnegative integer game


view this post on Zulip Darij Grinberg (Jan 04 2021 at 18:41):

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

view this post on Zulip Darij Grinberg (Jan 04 2021 at 18:42):

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

view this post on Zulip Kevin Buzzard (Jan 04 2021 at 18:42):

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

view this post on Zulip Darij Grinberg (Jan 04 2021 at 18:43):

aha

view this post on Zulip Darij Grinberg (Jan 04 2021 at 18:43):

it's part of mathlib?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 04 2021 at 18:44):

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

view this post on Zulip Bhavik Mehta (Jan 04 2021 at 18:44):

Darij Grinberg said:

it's part of mathlib?

Not yet, there's some open PRs though

view this post on Zulip 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)?

view this post on Zulip Kevin Buzzard (Jan 04 2021 at 18:56):

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

view this post on Zulip Aaron Anderson (Jan 04 2021 at 19:01):

(deleted)

view this post on Zulip 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.

view this post on Zulip Darij Grinberg (Jan 04 2021 at 19:07):

thank you!

view this post on Zulip 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)

view this post on Zulip 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