project management

Stream: mathlib4

[Steven Rossi]

Is there a reason why we don’t use projects more on the git? I seems like it’d be a nice way to organize getting to more complicated results and be more collaborative.

[Johan Commelin]

I don't understand your question. We use git and github a lot...

[Anatole Dedecker]

I think Steven is asking about the "projects" tab on GitHub

[Steven Rossi]

yep, just from a software development perspective, it seems a little cluttered with prs and it seems like developing fields like class field theory could benefit from a road map of sorts

[Ruben Van de Velde]

I think most people haven't tried working with them, but it would probably be fine if you wanted to use them for a project you're organising. Relatedly, are you aware of lean blueprints?

[Patrick Massot]

People try from time to time, but i never lasts long.

[Patrick Massot]

See https://github.com/orgs/leanprover-community/projects/9 for instance

[Steven Rossi]

Does lean have a system to outline future work besides sorry-ing everything :sweat_smile:

[Patrick Massot]

Yes, the Lean blueprint tool.

[Steven Rossi]

Do you have a link to read up on it?

[Patrick Massot]

It is mentioned very briefly at the end of https://arxiv.org/abs/2210.07746, but the main point is to see it in action, at https://leanprover-community.github.io/sphere-eversion/blueprint/index.html or https://leanprover-community.github.io/flt-regular/ for instance.

[Patrick Massot]

A crucial point is https://leanprover-community.github.io/flt-regular/dep_graph_document.html

[Steven Rossi]

Cool thanks!

[Utensil Song]

@Steven Rossi You might also be interested in the topic of trying to make blueprint also work for Lean 4 ecosystem here, the prototype has a minimal example project which renders to this blueprint and jumps to this doc-gen4 document for formalized definitions/theorems, there is a slightly different UX from the Lean 3 blueprint which jumps to the Lean source code. Looking forward to your feedbacks.

[Utensil Song]

The blueprint is a cool design that helps one plan a big proof project in a divide-and-conquer manner, and after the formalization is done, it becomes a guide to the formalized Lean library from an informal mathematical exposition.

I was hoping for something that can make documents like "Proof outline" and "Proof document" in Isabelle AFP e.g. https://www.isa-afp.org/entries/Undirected_Graph_Theory.html and blueprint is the closest thing, possibly it's a more advanced design that can make formalization a larger scale of semi-decentralized development practice.