portico: Add Lean case study.

templates/zerver/footer.html

@@ -43,6 +43,9 @@
             <li>
                 <a href="/case-studies/ucsd/">{{ _("University of California San Diego") }}</a>
             </li>
+            <li>
+                <a href="/case-studies/lean/">{{ _("Lean theorem prover community") }}</a>
+            </li>
         </ul>
     </div>
     <div class="footer-section">

templates/zerver/for/lean-case-study.md

@@ -0,0 +1,131 @@
+## Collaboration at the cutting edge of mathematics
+
+Modern mathematical research is an incredibly complex and specialized endeavor.
+Novel proofs may require years of dedicated study to understand, making it very
+difficult for the mathematical community to fully validate each other’s
+research. To enlist the help of computers for verifying mathematical theorems,
+mathematicians and computer scientists are [collaborating on an ambitious
+project](https://leanprover-community.github.io/) to develop the [Lean theorem
+prover](https://leanprover.github.io/) mathematics library.
+
+The Lean prover project was [featured in Nature magazine in June
+2021](https://www.nature.com/articles/d41586-021-01627-2), when an automated
+proof system was successfully used to [verify a result at the cutting edge of
+mathematical
+research](https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/).
+This accomplishment was the result of a deep multi-month collaboration between
+the [Lean Prover community](https://leanprover-community.github.io/) [on
+Zulip](https://leanprover.zulipchat.com/login/) and [Peter
+Scholze](https://www.hcm.uni-bonn.de/people/faculty/profile/peter-scholze/), a
+[world-famous mathematician](https://en.wikipedia.org/wiki/Peter_Scholze)
+working to “[rebuild much of modern
+mathematics](http://nature.com/articles/d41586-021-01627-2)”.
+
+“I joined the Zulip chat to answer any mathematical questions that may arise,
+but also as an interested spectator,” wrote Peter Scholze in a [blog post
+describing the
+project](https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/).
+“It was exactly the interactions via the Zulip chat that convinced me that a
+proper verification was going on," he commented.
+
+
+> “It was exactly the interactions via the Zulip chat that convinced me that a
+> proper verification was going on.”
+>
+> — [Peter Scholze](https://www.hcm.uni-bonn.de/people/faculty/profile/peter-scholze/),
+> professor at the [University of
+> Bonn](https://en.wikipedia.org/wiki/University_of_Bonn) and director at the
+> [Max Planck Institute for
+> Mathematics](https://en.wikipedia.org/wiki/Max_Planck_Institute_for_Mathematics)
+> ([source](https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/))
+
+“I have never seen this kind of collaboration before,” says [Kevin
+Buzzard](https://www.imperial.ac.uk/people/k.buzzard), Professor of Pure
+Mathematics at Imperial College London, who took part in Lean community’s
+verification effort. In mathematics, papers are generally coauthored by 2-3
+people who have known each other for years.  The verification project is
+breaking new ground, with 10 authors, most of whom have never met, scattered
+across the world. “Zulip has completely changed the way I work, and very much
+for the better,” says Kevin Buzzard, who also leads the [Xena
+project](https://xenaproject.wordpress.com/what-is-the-xena-project/) to
+formalize undergraduate mathematics with Lean and thereby transform how college
+mathematics is taught.
+
+
+## Unified library of mathematics developed by a diverse community
+
+Lean is an interactive theorem-prover and a programming language. Like C++ or
+Python, it would be impossible to use in practice without a library of
+pre-defined components — imagine writing a function from scratch every time you
+need to sort a list!  The functions that make it possible to “program” in Lean
+are being developed as
+[*mathlib*](https://github.com/leanprover-community/mathlib), a unified
+open-source library of mathematics.
+
+The mathlib development effort brings together a uniquely large and diverse
+group of contributors, ranging from renowned researchers to undergraduate
+students just starting their mathematical journey. The Zulip chat has been vital
+to attracting and growing the mathlib community, which has been the foundation
+of mathlib’s success.
+
+
+> “A number of people have cited the accessibility of [the Zulip] chat room as a
+> reason for deciding to use Lean.”
+>
+> — “The Lean Mathematical Library”, by the
+> [mathlib](https://github.com/leanprover-community/mathlib) community
+> ([arXiv:1910.09336v2](https://arxiv.org/abs/1910.09336v2) **[cs.LO])**
+
+Now numbering hundreds of active participants, the Lean community did not start
+out this way. [Launched in 2013](https://leanprover.github.io/about/), Lean was
+for many years developed by a small, tight-knit group, which exchanged ideas on
+a mailing list. Looking to have faster-paced interactions, the user community
+moved to Gitter in 2017, but it felt chaotic. Seeking a platform that would
+truly help the community to scale, the Lean community adopted Zulip in February
+2018.
+
+“When we moved to Zulip, it was instantly clear that the problems we were seeing
+on Gitter had gone away completely,” says [Kevin
+Buzzard](https://www.imperial.ac.uk/people/k.buzzard), Professor of Pure
+Mathematics at Imperial College London. “Zulip was incredibly intuitive to use.
+It just worked.”
+
+
+> “Zulip is incredibly intuitive.”
+>
+> — [Kevin
+> Buzzard](https://www.imperial.ac.uk/people/k.buzzard), Professor of Pure
+> Mathematics at Imperial College London
+
+
+## Accessible and efficient like no other chat platform
+
+Zulip’s unique combination of [topic-based
+organization](/why-zulip/) with a casual chat app feel helps
+the Lean community create a welcoming environment for newcomers. By [browsing
+recent topics](/help/recent-topics), newcomers can see what’s
+being discussed without being overwhelmed. They can start a new topic to ask
+basic questions without worrying about interrupting other conversations. Zulip’s
+threading model makes managing conversations incredibly efficient, allowing more
+senior community members to collaborate on research and library development, and
+jump in to help newer community members as time allows.
+
+
+> “We could never do what we’re doing on Slack or Discord.”
+>
+> — [Kevin Buzzard](https://www.imperial.ac.uk/people/k.buzzard), Professor of
+> Pure Mathematics at Imperial College London
+
+ “Zulip has been fantastic,” says [Robert Y. Lewis](https://robertylewis.com/),
+ Brown University lecturer and
+ [mathlib](https://github.com/leanprover-community/mathlib)
+ [maintainer](https://github.com/leanprover-community/mathlib#maintainers). “I
+ use Slack at work, and it works fine for 10-15 people, but I can’t imagine it
+ working at Lean’s scale.”
+
+
+> “I can’t imagine the Lean community without Zulip.”
+>
+> — [Robert Y. Lewis](https://robertylewis.com/), Brown University lecturer and
+> [mathlib](https://github.com/leanprover-community/mathlib)
+> [maintainer](https://github.com/leanprover-community/mathlib#maintainers)

templates/zerver/landing_nav.html

@@ -71,6 +71,9 @@
                         <li>
                             <a href="/case-studies/ucsd/">University of California San Diego</a>
                         </li>
+                        <li>
+                            <a href="/case-studies/lean/">Lean theorem prover community</a>
+                        </li>
                     </div>
                 </ul>
             </div>

templates/zerver/lean-case-study.html

@@ -0,0 +1,37 @@
+{% extends "zerver/portico.html" %}
+{% set entrypoint = "landing-page" %}
+
+{% block title %}
+<title>Case study: Lean theorem prover community</title>
+{% endblock %}
+
+{% block customhead %}
+<meta name="viewport" content="width=device-width, initial-scale=1.0" />
+{% endblock %}
+
+{% block portico_content %}
+
+{% include 'zerver/landing_nav.html' %}
+
+<div class="portico-landing why-page solutions-page case-study-page">
+    <div class="hero bg-education">
+        <div class="bg-dimmer"></div>
+        <div class="content">
+            <h1 class="center">Case study: <br/>Lean theorem prover community</h1>
+        </div>
+        <div class="hero-text">
+            Learn more about using Zulip for <a
+            href="/for/research">research</a><br/> and <a
+                                                         href="/for/open-source">open source</a> communities.
+        </div>
+    </div>
+    <div class="main">
+        <div class="padded-content">
+            <div class="inner-content markdown">
+                {{ render_markdown_path('zerver/for/lean-case-study.md') }}
+            </div>
+        </div>
+    </div>
+</div>
+
+{% endblock %}

zerver/tests/test_docs.py

@@ -159,6 +159,7 @@ class DocPageTest(ZulipTestCase):
         self._test("/for/open-source/", "for open source projects")
         self._test("/for/events/", "for conferences and events")
         self._test("/for/education/", "education pricing")
+        self._test("/case-studies/lean/", "Lean theorem prover")
         self._test("/case-studies/tum/", "Technical University of Munich")
         self._test("/case-studies/ucsd/", "UCSD")
         self._test("/for/research/", "for research")

zproject/urls.py

@@ -621,6 +621,7 @@ i18n_urls = [
     path("for/companies/", landing_view, {"template_name": "zerver/for-companies.html"}),
     path("case-studies/tum/", landing_view, {"template_name": "zerver/tum-case-study.html"}),
     path("case-studies/ucsd/", landing_view, {"template_name": "zerver/ucsd-case-study.html"}),
+    path("case-studies/lean/", landing_view, {"template_name": "zerver/lean-case-study.html"}),
     path(
         "for/communities/",
         landing_view,