formal roadmaps

Stream: maths

[Reid Barton]

I think we ought to collect "formal roadmaps" consisting of material which would be suitable for mathlib but with the more difficult proofs skipped, to serve as potential projects for new contributors. To this end and as a starting point for discussion I've created #1914.

[Reid Barton]

I have a couple more files in the works, but they depend on Urysohn's lemma, for which I intend to provide an actual proof.

[Rob Lewis]

IIRC we discussed something like this at Lean Together, right? It looks really nice. We might want to come up with guidelines for the roadmaps directory. Someone raised the idea of a place to store informal but very detailed proofs as blueprints for formalizations, and to encourage interested mathematicians to think about writing these things. Do you think that has a place alongside the formal roadmaps?

[Mario Carneiro]

I think the flypitch project used an informal roadmap (a 40 page tex document) IIRC

[Rob Lewis]

The cap set proof definitely did.

[Rob Lewis]

So we have a couple examples to start with.

[Kevin Buzzard]

Here's a roadmap to a non-trivial example of a perfectoid space. We didn't travel down the road yet but we'll get there in the end.