snapshot of https://github.com/zulip/zulip.git @ 48c69911c7dd4e03b20552eb3bd77ad8151c1357 (2026-09-15)

templates/corporate/case-studies/lean-case-study.md

@@ -0,0 +1,137 @@
+## 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 the interactive
+theorem prover 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 conversations](/help/recent-conversations), 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)
+
+---
+
+Check out our guides on using Zulip for [research](/for/research/)
+and [open source](/for/open-source/), and learn how Zulip
+[helps communities grow](/for/communities/)!