6.8 KiB
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 to develop the Lean theorem prover mathematics library.
The Lean prover project was featured in Nature magazine in June 2021, when an automated proof system was successfully used to verify a result at the cutting edge of mathematical research. This accomplishment was the result of a deep multi-month collaboration between the Lean Prover community on Zulip and Peter Scholze, a world-famous mathematician working to “rebuild much of modern mathematics”.
“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. “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, professor at the University of Bonn and director at the Max Planck Institute for Mathematics (source)
“I have never seen this kind of collaboration before,” says Kevin 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 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, 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 community (arXiv:1910.09336v2 [cs.LO])
Now numbering hundreds of active participants, the Lean community did not start out this way. Launched in 2013, 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, Professor of Pure Mathematics at Imperial College London. “Zulip was incredibly intuitive to use. It just worked.”
“Zulip is incredibly intuitive.”
— Kevin 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 with a casual chat app feel helps the Lean community create a welcoming environment for newcomers. By browsing 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, Professor of Pure Mathematics at Imperial College London
“Zulip has been fantastic,” says Robert Y. Lewis, Brown University lecturer and mathlib maintainer. “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, Brown University lecturer and mathlib maintainer
Check out our guides on using Zulip for research and open source, and learn how Zulip helps communities grow!