List of projects

Stream: general

[Terence Tao]

I wonder if this Zulip should have some persistent thread for listing active community formalization projects run on one of its channels; I am aware of PFR, PNT+, FLT, and now Carleson, but I do not know if this is the full list.

[Paige Thomas]

There is this listing, but I'm not sure if this covers what you are looking for.
https://leanprover-community.github.io/lean_projects.html

[Jeremy Tan]

Terence Tao said:

I wonder if this Zulip should have some persistent thread for listing active community formalization projects run on one of its channels; I am aware of PFR, PNT+, FLT, and now Carleson, but I do not know if this is the full list.

LTE

[Kevin Buzzard]

I'm not sure LTE is active. I know of at least one more project which is going to be announced soon.

[Joseph Myers]

Kayla Thomas said:

There is this listing, but I'm not sure if this covers what you are looking for.
https://leanprover-community.github.io/lean_projects.html

That page has lots of inactive Lean 3 projects and various projects that are single-person projects rather than run collaboratively on Zulip.

Now, many inactive and single-person projects (that are more than just someone's toy learning exercise) are certainly worth listing somewhere (and indeed somewhere curated, not just Reservoir). As well as being a showcase of the sort of things that have been done in Lean, they may well be a useful source of material to update and add to mathlib, or of ideas for future projects. So maybe an update of that page for Lean 4 shouldn't necessarily remove the old projects (although the table of supported Lean 3 versions for each project could perhaps go away), but rather (a) add lots more projects (active or otherwise) and (b) add key metadata such as "is this a community formalization project?", "is this project active?" (or "last commit date") and "what is the status of merging material from this project to mathlib, if it might be appropriate to do so?".

[Notification Bot]

5 messages were moved here from #announce > Carleson project by Floris van Doorn.

[Jon Eugster]

I think as with many documentation pages it's just a question of finding somebody who cares enough about it to take on the responsibility and keep it updated.I'm sure the community website would very much apprechiate such PRs!

[Julian Berman]

(deleted)

[Yury G. Kudryashov]

The compatibility matrix on that page is all about Lean 3

[Jeremy Tan]

We're still missing a lot of people for the Carleson project. We need more of them!

[Jeremy Tan]

(Much more.)