Zulip Chat Archive

Stream: maths

Topic: formal roadmaps


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jan 28 2020 at 10:26):

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

view this post on Zulip Rob Lewis (Jan 28 2020 at 10:29):

The cap set proof definitely did.

view this post on Zulip Rob Lewis (Jan 28 2020 at 10:29):

So we have a couple examples to start with.

view this post on Zulip 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