mirror of https://github.com/zulip/zulip.git
138 lines
6.8 KiB
Markdown
138 lines
6.8 KiB
Markdown
## 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 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)
|
||
|
||
---
|
||
|
||
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)!
|