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