# Zulip Chat Archive

## Stream: maths

### Topic: formal roadmaps

#### Reid Barton (Jan 27 2020 at 23:06):

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 (Jan 27 2020 at 23:06):

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 (Jan 28 2020 at 10:25):

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 (Jan 28 2020 at 10:26):

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

#### Rob Lewis (Jan 28 2020 at 10:29):

The cap set proof definitely did.

#### Rob Lewis (Jan 28 2020 at 10:29):

So we have a couple examples to start with.

#### Kevin Buzzard (Jan 28 2020 at 12:14):

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.

Last updated: May 09 2021 at 10:11 UTC