Parallelizing formalization efforts?

Stream: new members

[Alexander Heckett]

Hello everyone!

I'm working on some game theory research and I'd like to formalize my work in Lean -- in particular I'd like some kind of von Neumann minimax theorem to exist in Mathlib. As far as I can tell the most canonical approach is to:

(1) Compute some homology groups of spheres
(2) Use sphere homologies to prove Brouwer's fixed point theorem
(3, optional) Use Brouwer's fixed point theorem to prove Kakutani's fixed point theorem.
(4) Use either Brouwer's fixed point theorem or Kakutani's fixed point theorem to prove von Neumann's minimax theorem.

Based on other conversations on this site, it seems that step (1) alone may take a long time. All of these steps seem fairly parallelizable. Is there a way for people to start working on later steps while the earlier steps are still being proven? (Sorry about being totally ignorant of the habits of the mathlib community -- very new here.)

[Ruben Van de Velde]

The main thing that is not possible is to check results into mathlib that rely on other not-yet-formalized results (unless in the shape of "this result implies that result", but that's likely not what we'd want). If that's what you want to do, you can set up a project outside mathlib for as long as you're in that situation

[Johan Commelin]

We can parallelise using https://en.wikipedia.org/wiki/Eilenberg-Steenrod_axioms

[Johan Commelin]

That is more along the "this result implies that result" lines