2021-11-05 21:35:41 +01:00
|
|
|
|
## 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
|
2022-01-19 21:01:56 +01:00
|
|
|
|
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
|
2021-11-05 21:35:41 +01:00
|
|
|
|
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
|
2021-11-24 21:55:00 +01:00
|
|
|
|
proper verification was going on,” he commented.
|
2021-11-05 21:35:41 +01:00
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
> “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
|
|
|
|
|
|
|
2022-01-19 21:01:56 +01:00
|
|
|
|
Lean is an interactive theorem prover and a programming language. Like C++ or
|
2021-11-05 21:35:41 +01:00
|
|
|
|
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)
|
2021-11-11 07:37:26 +01:00
|
|
|
|
|
|
|
|
|
|
---
|
|
|
|
|
|
|
|
|
|
|
|
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)!
|
