Announcing the proof clinic!

Stream: Leaning In!

[Jesse Alama]

The program for Leaning In! 2025 is shaping up nicely. We have five talks lined up so far, and there's space for a couple more.

I'm excited to flag one item in particular, which is the Proof Clinic. The intention of the proof clinic is for participants to show us where they're stuck with Lean, or having trouble, and work with the group to try to get unstuck. No promises, but we'll try! Topics can be as complicated as "How do I choose between competing definitions?" to "How do I install Lean?" See the program for more details.

[Joachim Breitner]

I wish “How do I install Lean” weren't an example for a complicated question! :man_facepalming:

[Jesse Alama]

I also hope that "How do I install Lean?" doesn't really arise as a question -- it was a bit tongue-in-cheek! The intention is that all questions and requests for help are welcome, even for topics where we might be a bit embarrased to admit we're stuck...

[Yves Jäckle]

Does one receive a confirmation mail after registering ? :sweat_smile:

[Jesse Alama]

Yves Jäckle said:

Does one receive a confirmation mail after registering ? :sweat_smile:

Sent! Sorry for the delay. Unfortunately, when I set up the form, I didn't realize that it would be a manual process on my part to send out a confirmation. I saw your registration (and yours too, @Michael Rothgang ).

[Berber]

I am looking to implement abstract simplicial complexes into lean, of course aiming to have it in mathlib.

Very open statement, I know. Who can/wants to help me?

[Johan Commelin]

FYI: there is docs#Geometry.SimplicialComplex and docs#SSet .
But maybe you were already aware of those.

[Johan Commelin]

And there is also a lot of discussion at #maths > Abstract Simplicial Complex

[Berber]

thanks! these are less abstract simplicial complexes, and are within the context of more geometrical settings. simplicial sets are not the same as simplicial complexes, though of course very related. i want to define abstract simplicial complexes.

i did not know about the discussion you linked, thanks, that is very helpful!