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:
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:
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