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

## 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)!