Roadmap

Stream: mathlib4

[Josha Dekker]

Is there some kind of “formalization roadmap” that pins down a “main road” to develop results in a particular area of math? I’m not even exactly sure what I mean by this question, and I’m sure that there won’t be a “one-size-fits-all” solution, but I guess I’m wondering if there is some agreement along the lines of “in field X, we should probably tackles problems A, B…. Z in roughly this order (in particular, pointing out what levels of generality we should start off with for these problems), where we may want to formalize concepts 1,…,10 somewhat like …”? I guess that having such a layout may help people take shots at small bits that they are interested in/have knowledge on, without having knowledge in all subdomain. Also, it is a nice way to keep track of how far some aspects of the theory are formalized. If this is not yet the case, would it be interesting to see if some agreement can be reached for some areas of maths (eg by domain experts and formalization experts)?

[Josha Dekker]

A tool like Blueprint may help to give such a roadmap a more tangible shape, where perhaps the shape of the roadmap gets updated as new insights appear/roadblocks are discovered?

[Yury G. Kudryashov]

Some people have roadmaps towards results they care about in their head.

[Jeremy Tan]

Like me.

[Yury G. Kudryashov]

If you want to work towards a specific goal, then you can ask here (in a new thread) and probably there will be an expert in that area who will help with the roadmap.

[ZHAO Jiecheng]

It might be good to share blueprints with each other first. But I have no idea how people would organize them yet. But you may know other's roadmap through the blueprints.
@Yury G. Kudryashov Is there any blueprints of Mathlib now?

[Yury G. Kudryashov]

AFAIK, no.

[Yury G. Kudryashov]

Currently, every contributor works on something they care about. No formal project goals etc.

[Yury G. Kudryashov]

Some people come, contribute definitions/theorems. If the maintainers consider them relevant and well-written, then they're accepted to the library.

[Josha Dekker]

I get that, thanks! What I was thinking is more along the following line of thought: persons A and B want to work on projects A and B respectively. Using their respective personal roadmaps, the projects will take some given amount of time. If both projects have large overlaps/can be approached to have large overlaps, a slightly different approach for either project may individually lengthen each project. However, this may generate a lot of useful results for the other project, substantially shortening that project; this leads to a net improvement.

With this logic in mind, I was wondering if it would be interesting to map out some N interesting/important results in a given field, and map out a roadmap that allows us to formalize these N results “efficiently”: this will probably introduce some more need for discussions about these topics, but it might help to increase development speed in the long run!