Saintan Wu

Stream: new members

[Saintan Wu]

Hello I'm new to Lean and I'm interested in Graph theory. I'm seeing there's several todos in the graph theory stream and wondering if there is something I can help.

[Arthur Paulino]

Hello @Saintan Wu!
Kyle and Yael are planning out a refactoring/optimization of the graph API. I am not sure where things are going because I am new to Lean as well :D.
In the meantime, you might want to subscribe to #graph theory and get yourself more comfortable with the combinatorics.simple_graph.basic API.

[Yaël Dillies]

Yes, I'm currently busy setting up multigraphs, busy designing the upcoming graph refactor and busy doing all the other random stuff I can procrastinate with.
Feel free to tackle anything on the TODO lists. Unless they ask for structural changes, they should not conflict with the aforementioned agitation.

[Saintan Wu]

Thanks a lot! I will then look more around and maybe try Sperner's Lemma later.

[Yaël Dillies]

Sperner's lemma? or Sperner's theorem? Either way, I'm sorry but we did them both :grinning_face_with_smiling_eyes:. Sperner's theorem lives on branch#combinatorics and Sperner's lemma is almost done at branch#sperner-again.

[Ruben Van de Velde]

So what would mathlib style be? lemma sperners_theorem and theorem sperners_lemma? :)

[Saintan Wu]

That's wonderful! I'll go find another things I can help with.