Combinatorics

Stream: new members

[John Talbot]

Hi, I'm interested in combinatorics, in particular extremal questions about hypergraphs.
I've only been using Lean for a couple of weeks so I would really appreciate any suggestions/tips as to where start - thanks!

[Mauricio Collares]

I think mathlib knows nothing about hypergraphs at the moment (other areas might use simplicial complexes and the like, but it wouldn't be hypergraphs as extremal people are used to them). Bhavik Mehta and Yaël Dillies did SzRL and triangle removal, but we don't even have Turán for graphs yet. I am working on it at the moment, but I am not dedicating a lot of time to it due to other commitments. I would be more than happy to dedicate more time to it and collaborate, though!

[Mauricio Collares]

What kinds of extremal hypergraph problems are you interested in?

[Mauricio Collares]

We have a #graph theory stream, by the way

[John Talbot]

Thanks for pointers! I've mainly worked on Turan-type questions and problems on intersecting families.

[Mauricio Collares]

Ah, I think @Yaël Dillies has been formalizing some theorems about set systems recently.

[Mauricio Collares]

I guess even Erdős-Ko-Rado would be a nice project, especially if you have your favorite follow-up to it.

[Yaël Dillies]

#2770 for Erdős-Ko-Rado

[Yaël Dillies]

Hey! On intersecting families there is #14475, #14497 and #14543 open. I'm currently working on shattering families and the Sauer-Shelah lemma. I am coaching a friend to do the Ahlswede-Zhang identity and the overall plan is to have all the Cambridge Combinatorics course formalised.

[John Talbot]

Thanks that looks very interesting!