Sperner's lemma

[YaelDillies]

Sperner's lemma is a combinatorial statement about some colorings of the triangulations of a triangle. It can be used to prove the Brouwer fixed point theorem.

Bhavik and I had a go at implementing Sperner's lemma in Lean 3 back in 2021 (in fact, Bhavik had an even earlier go). We reduced the problem to some combinatorial statement with geometric input, and found a proof of it, but the effort petered out before that proof was formalised.

I would be happy to supervise someone to take over where we left things off.

[b-mehta]

Likewise happy to help out with this. The geometric input should now be in mathlib, and so this should be not too hard to finish off.

[metakunt]

I could try it out if the math involved is fairly elementary.

[YaelDillies]

The worse you need to deal with is some convex combination nonsense :)

[metakunt]

As long as I don't need tons of books in category theory/algebraic geometry as a prerequisite. Can you send me the statements on zulip?

[YaelDillies]

Here is the statement of Sperner's lemma: https://github.com/YaelDillies/MiscYD/blob/master/MiscYD/Convexity/Sperner/Sperner.lean

Note that I haven't ported from Lean 3 the reduction to convex geometry. You can try to figure it for yourself with or without looking at the Lean 3 code.

If you are not interested in doing the reduction to convex geometry, please tell me and wait a few weeks for me to port it from Lean 3.

[metakunt]

Ok, I wrote you on zulip for some clarifications.