Zulip Chat Archive

Stream: new members

Topic: Saintan Wu


Saintan Wu (Dec 25 2021 at 05:52):

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 (Dec 25 2021 at 23:31):

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 (Dec 25 2021 at 23:57):

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 (Dec 26 2021 at 01:43):

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

Yaël Dillies (Dec 26 2021 at 09:52):

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 (Dec 26 2021 at 09:58):

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

Saintan Wu (Dec 27 2021 at 03:29):

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


Last updated: Dec 20 2023 at 11:08 UTC