Any ideas for a formalization project?

Stream: new members

[Benoît Guillemet]

Hello, I am a student in my first year of a master's degree in mathematics at ENS Paris-Saclay, France. Some friends and I would like to work on a small formalization project in Lean. Thus, we are searching for a theorem to formalize that is understandable at our level and that is not in Mathlib for the moment (so that our work might be useful).
Our areas of interest are geometry, algebraic topology, and category theory. We could also formalize a result in combinatorics, graph theory, or logic.
Does anyone have any ideas?

[Kevin Buzzard]

Singular homology!

[Kevin Buzzard]

The definition we use is quite "category-theoretic", and there is plenty of low-hanging fruit (like singular homology of basic spaces such as n-space or the n-sphere). Better check amongst the experts that this is not yet (a) done or (b) being worked on, but I am pretty sure that we're ready for it and it would be very cool to have it.

[Kevin Buzzard]

here is Massot talking about it last November; since then Riou has finished his refactor of homological algebra so I think we're ready. Both Massot and Riou are at Saclay.

[Johan Commelin]

Patrick Massot is Pittsburgh for the rest of this academic year.

[Adam Topaz]

There are also lots of people thinking about formalizing infinity category theory, so I’m sure some projects in this field would be both interesting and useful

[Patrick Massot]

Bonjour Benoît ! How much time do you want to spend on this? One project that some students here in CMU worked on but did not finish is formalizing Milnor's proof of the hairy ball theorem. It is a geometric proof of an algebraic topology result so it fits your list, and it is much more elementary than infinity category theory. I think it would be a very nice project.

[Anatole Dedecker]

Another thing that would be nice would be to help develop the theory of covering maps (if my calculations are correct and if you indeed follow his course, I think Frédéric Paulin should start telling you about it either this week or next week :wink:). But people have been thinking about this so there's a higher collision risk I would say.

[Anatole Dedecker]

For example it could be relatively easy and very helpful to build the theory of proper group actions on top of docs#IsProperMap, which will also be somewhat related to Frédéric Paulin's course. That's probably less fun than the hairy ball theorem though!

[Adam Topaz]

I'm not familiar with Milnor's proof of the hairy ball theorem, but certainly the proof via the Euler characteristic would introduce various things which are worthwhile to have independently of that theorem.

[namibj]

I'm not sure if this is out-of-scope, but formalization should help with verifying the impact of architectural modifications:
https://www.semanticscholar.org/paper/Signal-Propagation-in-Transformers%3A-Theoretical-and-Noci-Anagnostidis/5eeb80dc67590422db64ca95ec0aded24799cfb6

[namibj]

(I'd love a classification of this along this sort of schema, though, if anyone would like to teach me.)

[Benoît Guillemet]

Thank you for all your answers!
I think the most doable project for us among the ones you proposed is either one of the proofs of the hairy ball theorem or some results in the theory of covering maps. The idea is only to spend a few hours a week in our spare time to have fun with Lean, so even the basics of singular homology seem a little too big. How can I know if people are already working on covering maps?
I will discuss that with the people who want to get into this project with me and keep you informed of what we choose!

[Anatole Dedecker]

If I remember correctly, @Junyan Xu was working on this actively (e.g in #7596, which I should go back to reviewing now that my semester is finished). I'll try to find the last thread about it.

[Anatole Dedecker]

Here is the thread: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Path.20lifting

Reading it again it seems that a few people have proven the path/homotopy lifting property already, so it's not a good idea to do one more proof. On the other hand, if we can manage to get that merged relatively soon then you could build on top of it.

[Anatole Dedecker]

I think with enough organization we should be able to split the work so that no one steps on other's people toes, if you are interested we could open another thread about it.

[Anatole Dedecker]

By the way I'd be really happy to talk about this IRL if you want, whatever you end up working on! Most of my courses are in Paris this semester, but I should still be in Orsay relatively frequently (I'm in M2 AAG).

[Scott Carnahan]

Here's an unformalized fact that might go in interesting directions: a "Hopf algebra object" in the category of sets is the same thing as a group. Here, the "comultiplication" is necessarily the diagonal embedding.

[Benoît Guillemet]

Anatole Dedecker said:

By the way I'd be really happy to talk about this IRL if you want, whatever you end up working on! Most of my courses are in Paris this semester, but I should still be in Orsay relatively frequently (I'm in M2 AAG).

Thank you for the details. It would indeed be really nice if we could meet you and ask you a few questions IRL (maybe we can talk about this in dm)!

Scott Carnahan said:

Here's an unformalized fact that might go in interesting directions: a "Hopf algebra object" in the category of sets is the same thing as a group. Here, the "comultiplication" is necessarily the diagonal embedding.

Thank you for your proposition!

We finally chose to start with a proof of the hairy ball theorem, but this is only the beginning.

[Patrick Massot]

I guess you found it already but the proof I had in mind is https://www.jstor.org/stable/2320860

[Junyan Xu]

If you'd like projects around covering spaces and fundamental groups, take a look at the "Planned" tab of the Covering spaces and étale spaces project; I just added a detailed outline towards the Van Kampen theorem. Constructing the monodromy of a covering map and proving the lifting criterion should also be quite straightforward given what's already in #10084. I'm not sure I'll find time to work on them in the near future, but I'll certainly be happy to answer questions and review PRs.
(Update: I've added links to some PRs/branches that I've started but not finished.)

[Benoît Guillemet]

Patrick Massot said:

I guess you found it already but the proof I had in mind is https://www.jstor.org/stable/2320860

Thank you! We are currently studying the different proofs to determine which is most interesting for us to formalize.

Junyan Xu said:

If you'd like projects around covering spaces and fundamental groups, take a look at the "Planned" tab of the Covering spaces and étale spaces project; I just added a detailed outline towards the Van Kampen theorem. Constructing the monodromy of a covering map and proving the lifting criterion should also be quite straightforward given what's already in #10084. I'm not sure I'll find time to work on them in the near future, but I'll certainly be happy to answer questions and review PRs.
(Update: I've added links to some PRs/branches that I've started but not finished.)

Thank you for your answer. For the moment, we're going to work on the hairy ball theorem, but we may come back to you later.

[Patrick Massot]

Milnor's proof is a cute elementary proof but the downside is that it leaves you with no understanding of why the theorem is true and no tool to prove more results. The principled way of proving this result is to build an algebro-topological invariant that can be computed using any vector field. Say you manage to define the Euler characteristic of a manifold and prove that every vector field which vanishes transversely can be used to compute the Euler characteristic. Then you can compute the Euler characteristic of even-dimensional spheres using your favorite explicit vector field and get $2$ and argue that a nowhere vanishing vector field would allow to prove $0 = 2$ in $\Z$. But this is a lot more work to formalize than Milnor's proof.

[Benoît Guillemet]

Ok, so I guess Milnor's proof should be more reasonable to begin with.
I also found another proof using homology that seems a bit more elementary than the one you described. Assuming there exists a non-vanishing vector field $v$, you could get a homotopy between the identical map and the antipodal map on $S^n$ with $H(x,t) = \cos(\pi t)x + \sin(\pi t)v(x)$. As the degree of the antipodal map is $-1$ as long as $n$ is even, you can derive a contradiction. However, I don't know if the degree of a map $S^n \rightarrow S^n$ is already formalized in Lean or not. It could be quite hard to do depending on what is already in mathlib and what isn't.

[Patrick Massot]

This is also a nice proof but indeed it requires degree theory which is not trivial to setup either.

[Kevin Cheung]

I would like to see a formalized proof of the Perfect Graph Theorem.

[Mauricio Collares]

The Lovász one or the strong one?

[Kevin Cheung]

The Strong Perfect Graph Theorem.

[Kevin Cheung]

That will probably take years of work though. Maybe the Weak Perfect Graph Theorem is a good start since it's already done in Coq. https://arxiv.org/abs/1912.02211

[Benoît Guillemet]

We finally chose to work on Milnor's proof to begin with something simple. We are supervised by @Anatole Dedecker, so everything should go well!

Kevin Cheung said:

I would like to see a formalized proof of the Perfect Graph Theorem.

Thank you for your suggestion. It may be for another project.