From e7c5f0acba2059eec2b7667b4720837ed9a86d7d Mon Sep 17 00:00:00 2001 From: faenuccio Date: Fri, 26 Jun 2026 19:37:57 +0200 Subject: [PATCH 1/6] first commit --- templates/lean_projects.html | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/templates/lean_projects.html b/templates/lean_projects.html index 535067eec2..4069697e15 100644 --- a/templates/lean_projects.html +++ b/templates/lean_projects.html @@ -5,12 +5,22 @@

Lean projects

+More and more projects formalizing mathematical results in Lean are being pursued, and in this page we list both projects that we qualify as "intentions" and more structured ones. Although there is no clear barrier, the first list aims at avoiding work duplication and to inform colleagues that someone is already planning to actively work on formalizing a certain topic. The second list, hosted on Reservoir, is an up-to-date and thorough index of all public open-source Lean projects. + +

Intentions

+

- Reservoir is an up-to-date and thorough index of all public open-source Lean projects. +We use the "intentions registration" mechanism from [`leanprover-community/intentions`](https://github.com/leanprover-community/intentions), +and the shared public registry of intentions at [`leanprover-community/project-intentions`](https://github.com/leanprover-community/project-intentions). Everyone is free to add their project to the registry: there is no scientific moderation, but we ban all projects making use of discriminatory or violent language and, more generally, of all expressions that violate the [Contributor Covenant Code of Conduct](https://www.contributor-covenant.org/version/2/0/code_of_conduct/). We see this registry as an opportunity for colleagues to be informed that someone is already working on a specific project, allowing for coordination, collaboration and respect of good academic practices. We are not responsible for potential conflicts that might result in cases of duplication, overlapping or plagiarism. We encourage all contributors to register to our [Zulip Chat](https://leanprover.zulipchat.com/) and to engage in conversation with the whole community: we see registering an intention and discussing it on Zulip as complementary actions and we expect most contributors to set up both.

- On this page we list a representative sample of projects that depend on Mathlib. +There's a special bar for student projects. It's really important that students are "left to work in peace" to the extent possible. Common sense will be required here (a student project "I'm going to do Sobolev spaces" or "differential geometry" are very general, and we suggest to be more specific), and we invite the wider community to participate in getting this right. +

+ +

Open-source Lean projects

+

+ The following is a representative sample of projects that depend on Mathlib. To add a project to this list, you can add it to downstream-repos.yml in Mathlib.

@@ -36,8 +46,8 @@
maintained by {% endfor %} - -

Lean 3 projects

+ +

Lean 3 projects

The projects listed below were made for the outdated Lean 3, and today are of historical interest only. From 2a7a8170cd8655e2fbe3b80e0fc3148fd5073d61 Mon Sep 17 00:00:00 2001 From: faenuccio Date: Thu, 2 Jul 2026 16:16:34 +0200 Subject: [PATCH 2/6] updated url --- templates/lean_projects.html | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/templates/lean_projects.html b/templates/lean_projects.html index 4069697e15..28781120ba 100644 --- a/templates/lean_projects.html +++ b/templates/lean_projects.html @@ -10,8 +10,7 @@

Lean projects

Intentions

-We use the "intentions registration" mechanism from [`leanprover-community/intentions`](https://github.com/leanprover-community/intentions), -and the shared public registry of intentions at [`leanprover-community/project-intentions`](https://github.com/leanprover-community/project-intentions). Everyone is free to add their project to the registry: there is no scientific moderation, but we ban all projects making use of discriminatory or violent language and, more generally, of all expressions that violate the [Contributor Covenant Code of Conduct](https://www.contributor-covenant.org/version/2/0/code_of_conduct/). We see this registry as an opportunity for colleagues to be informed that someone is already working on a specific project, allowing for coordination, collaboration and respect of good academic practices. We are not responsible for potential conflicts that might result in cases of duplication, overlapping or plagiarism. We encourage all contributors to register to our [Zulip Chat](https://leanprover.zulipchat.com/) and to engage in conversation with the whole community: we see registering an intention and discussing it on Zulip as complementary actions and we expect most contributors to set up both. +We rely on the registry of [project intentions](https://github.com/orgs/leanprover-community/projects/34/views/1) to keep track of ongoing projects. Everyone is free to add their project to the registry: there is no scientific moderation, but we ban all projects making use of discriminatory or violent language and, more generally, of all expressions that violate the [Contributor Covenant Code of Conduct](https://www.contributor-covenant.org/version/2/0/code_of_conduct/). We see this registry as an opportunity for colleagues to be informed that someone is already working on a specific project, allowing for coordination, collaboration and respect of good academic practices. We are not responsible for potential conflicts that might result in cases of duplication, overlapping or plagiarism. We encourage all contributors to register to our [Zulip Chat](https://leanprover.zulipchat.com/) and to engage in conversation with the whole community: we see registering an intention and discussing it on Zulip as complementary actions and we expect most contributors to set up both.

From 43612dce25645d382365a306d15936b5d6c6a1bb Mon Sep 17 00:00:00 2001 From: faenuccio Date: Mon, 6 Jul 2026 15:18:13 +0200 Subject: [PATCH 3/6] Kim's comments --- templates/lean_projects.html | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/templates/lean_projects.html b/templates/lean_projects.html index 28781120ba..25d6cadcda 100644 --- a/templates/lean_projects.html +++ b/templates/lean_projects.html @@ -5,23 +5,28 @@

Lean projects

-More and more projects formalizing mathematical results in Lean are being pursued, and in this page we list both projects that we qualify as "intentions" and more structured ones. Although there is no clear barrier, the first list aims at avoiding work duplication and to inform colleagues that someone is already planning to actively work on formalizing a certain topic. The second list, hosted on Reservoir, is an up-to-date and thorough index of all public open-source Lean projects. +There are many active projects formalizing mathematical results in Lean. On this page we provide a list of established projects using Mathlib, and also a list of early stage projects (or even just intentions for projects). This second list is useful for avoiding duplication, making sure you don't scoop student projects, or finding collaborators.

Intentions

-We rely on the registry of [project intentions](https://github.com/orgs/leanprover-community/projects/34/views/1) to keep track of ongoing projects. Everyone is free to add their project to the registry: there is no scientific moderation, but we ban all projects making use of discriminatory or violent language and, more generally, of all expressions that violate the [Contributor Covenant Code of Conduct](https://www.contributor-covenant.org/version/2/0/code_of_conduct/). We see this registry as an opportunity for colleagues to be informed that someone is already working on a specific project, allowing for coordination, collaboration and respect of good academic practices. We are not responsible for potential conflicts that might result in cases of duplication, overlapping or plagiarism. We encourage all contributors to register to our [Zulip Chat](https://leanprover.zulipchat.com/) and to engage in conversation with the whole community: we see registering an intention and discussing it on Zulip as complementary actions and we expect most contributors to set up both. +The [project intentions](https://github.com/orgs/leanprover-community/projects/34/views/1) registry keeps track of projects at earlier stages (including ones that have barely started). Everyone is free to add their project, and there are no guarantees that the registry covers everything that is happening. There's very limited scientific moderation of the list, but of course the [Community Guidelines](https://leanprover-community.github.io/community_guidelines.html) apply here too. + +The registry is an opportunity to inform others in the community of your intentions, allowing for coordination, collaboration, and respect of good academic practices. There are no guarantees here: many projects are not registered, and we enforce no control to avoid that people start working on projects registered by others. We hope, nevertheless, that this registry will encourage and enable a collaborative and cooperative approach. We encourage everyone to participate in the [Lean Zulip Chat](https://leanprover.zulipchat.com/); project intentions are complementary to discussion on Zulip, not a replacement.

-There's a special bar for student projects. It's really important that students are "left to work in peace" to the extent possible. Common sense will be required here (a student project "I'm going to do Sobolev spaces" or "differential geometry" are very general, and we suggest to be more specific), and we invite the wider community to participate in getting this right. -

- -

Open-source Lean projects

+There's a special bar for student projects. It's really important that students are "left to work in peace". Common sense will be required here (a student project "I'm going to do Sobolev spaces" or "differential geometry" are very general, and we suggest to be more specific), and we invite the wider community to participate in getting this right. +

Open-source projects using Mathlib

The following is a representative sample of projects that depend on Mathlib. To add a project to this list, you can add it to downstream-repos.yml in Mathlib.

+

+ You can also find a list of most open-source projects using Lean on Reservoir. +

+ To add a project to this list, you can add it to downstream-repos.yml in Mathlib. +

{% for project in projects_4 %} From d3921e52509049c69ad43546b657252bb77db406 Mon Sep 17 00:00:00 2001 From: faenuccio Date: Thu, 9 Jul 2026 20:10:40 +0200 Subject: [PATCH 4/6] modified main link to the general repository. --- templates/lean_projects.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/templates/lean_projects.html b/templates/lean_projects.html index 25d6cadcda..4f45468ceb 100644 --- a/templates/lean_projects.html +++ b/templates/lean_projects.html @@ -10,7 +10,7 @@

Lean projects

Intentions

-The [project intentions](https://github.com/orgs/leanprover-community/projects/34/views/1) registry keeps track of projects at earlier stages (including ones that have barely started). Everyone is free to add their project, and there are no guarantees that the registry covers everything that is happening. There's very limited scientific moderation of the list, but of course the [Community Guidelines](https://leanprover-community.github.io/community_guidelines.html) apply here too. +The [project intentions](https://github.com/orgs/leanprover-community/projects/34/views/1) registry keeps track of projects at earlier stages (including ones that have barely started). Everyone is free to add their project, and there are no guarantees that the registry covers everything that is happening. To add new intentions to the registry, navigate to [the main page](https://github.com/leanprover-community/project-intentions) of that repository and follow the instructions. There's very limited scientific moderation of the list, but of course the [Community Guidelines](https://leanprover-community.github.io/community_guidelines.html) apply here too. The registry is an opportunity to inform others in the community of your intentions, allowing for coordination, collaboration, and respect of good academic practices. There are no guarantees here: many projects are not registered, and we enforce no control to avoid that people start working on projects registered by others. We hope, nevertheless, that this registry will encourage and enable a collaborative and cooperative approach. We encourage everyone to participate in the [Lean Zulip Chat](https://leanprover.zulipchat.com/); project intentions are complementary to discussion on Zulip, not a replacement.

From 2c01950cc4b177b8c77fa9861ba8adee29fe3f7a Mon Sep 17 00:00:00 2001 From: "Filippo A. E. Nuccio" Date: Wed, 15 Jul 2026 14:53:02 +0200 Subject: [PATCH 5/6] Apply suggestion from @grunweg Co-authored-by: Michael Rothgang --- templates/lean_projects.html | 1 + 1 file changed, 1 insertion(+) diff --git a/templates/lean_projects.html b/templates/lean_projects.html index 4f45468ceb..7f5f66b0d9 100644 --- a/templates/lean_projects.html +++ b/templates/lean_projects.html @@ -17,6 +17,7 @@

Intentions

There's a special bar for student projects. It's really important that students are "left to work in peace". Common sense will be required here (a student project "I'm going to do Sobolev spaces" or "differential geometry" are very general, and we suggest to be more specific), and we invite the wider community to participate in getting this right. +

Open-source projects using Mathlib

The following is a representative sample of projects that depend on Mathlib. From 3452fd1b9188d4c5242214d0bb5cf45c3cb28d65 Mon Sep 17 00:00:00 2001 From: "Filippo A. E. Nuccio" Date: Wed, 15 Jul 2026 14:53:53 +0200 Subject: [PATCH 6/6] Apply suggestions from code review Co-authored-by: Michael Rothgang --- templates/lean_projects.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/templates/lean_projects.html b/templates/lean_projects.html index 7f5f66b0d9..4ce70518de 100644 --- a/templates/lean_projects.html +++ b/templates/lean_projects.html @@ -10,7 +10,7 @@

Lean projects

Intentions

-The [project intentions](https://github.com/orgs/leanprover-community/projects/34/views/1) registry keeps track of projects at earlier stages (including ones that have barely started). Everyone is free to add their project, and there are no guarantees that the registry covers everything that is happening. To add new intentions to the registry, navigate to [the main page](https://github.com/leanprover-community/project-intentions) of that repository and follow the instructions. There's very limited scientific moderation of the list, but of course the [Community Guidelines](https://leanprover-community.github.io/community_guidelines.html) apply here too. +The [project intentions](https://github.com/orgs/leanprover-community/projects/34/views/1) registry keeps track of projects at earlier stages (including ones that have barely started). Everyone is free to add their project, but there are no guarantees that the registry covers everything that is happening. To add new intentions to the registry, navigate to [the main page](https://github.com/leanprover-community/project-intentions) of that repository and follow the instructions. There's very limited scientific moderation of the list, but of course the [Community Guidelines](https://leanprover-community.github.io/community_guidelines.html) apply here too. The registry is an opportunity to inform others in the community of your intentions, allowing for coordination, collaboration, and respect of good academic practices. There are no guarantees here: many projects are not registered, and we enforce no control to avoid that people start working on projects registered by others. We hope, nevertheless, that this registry will encourage and enable a collaborative and cooperative approach. We encourage everyone to participate in the [Lean Zulip Chat](https://leanprover.zulipchat.com/); project intentions are complementary to discussion on Zulip, not a replacement.