Add intentions to the project page

templates/lean_projects.html

@@ -5,12 +5,27 @@
 
     <h1>Lean projects</h1>
 
+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.
+
+    <h2>Intentions</h2>
+
     <p>
-      <a href="https://reservoir.lean-lang.org/">Reservoir</a> is an up-to-date and thorough index of all public open-source Lean projects.
+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.
     </p>
 
     <p>
-      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". 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. 
+
+    <h2>Open-source projects using Mathlib</h2>
+    <p>
+      The following is a representative sample of projects that depend on Mathlib.
+      To add a project to this list, you can add it to <a href="https://github.com/leanprover-community/mathlib4/blob/master/scripts/downstream_repos.yml">downstream-repos.yml</a> in Mathlib.
+    </p>
+    <p>
+      You can also find a list of most open-source projects using Lean on <a href="https://reservoir.lean-lang.org/">Reservoir</a>.
+    </p>
       To add a project to this list, you can add it to <a href="https://github.com/leanprover-community/mathlib4/blob/master/scripts/downstream_repos.yml">downstream-repos.yml</a> in Mathlib.
     </p>
 
@@ -36,8 +51,8 @@ <h6 class="card-subtitle mb-2 text-muted">maintained by
       </div>
     {% endfor %}
     </div>
-
-    <h1>Lean 3 projects</h1>
+    
+    <h2>Lean 3 projects</h2>
 
     <p>
       The projects listed below were made for the outdated Lean 3, and today are of historical interest only.