The Magic is People
29 Sept 2025
About a decade ago my dad, a United Methodist minister, was in a room with about a dozen other Methodist ministers working on some policy document, something he had probably done hundreds of times in his career. This time, someone projected a Google doc at the front of the room, and all the other people in the room had the document open on their laptops in edit mode, allowing them to collaborate by discussing changes, or by just making changes directly.
The excitement Dad expressed as he related this experience really stuck with me. He was describing technology that I was familiar with and that I’d used dozens of times. I believed Google Docs was built with care and a high level of craftsmanship, but it wasn’t, like, fundamentally that exciting to me. But Dad wanted me to understand that, from his perspective, there was something important and new here, something that he wished more people knew about. Google Docs’s multiplayer collaborative editing allowed his group to work together in a different way than anything he had encountered before.
There was, for lack of a better word, some magic for him in this way of using Google Docs.
It was, and still is, pretty clear to me that the well-designed, well-executed, senior-Methodist-minister-friendly software was not the magic thing. The software was important as a catalyst, but the magic was in the people and the way they were able to work together with the help of the technology.
Anyway, three weeks ago I joined the organization that is developing a programming language called Lean. The story about my dad is true, and it is also a parable. Lean is exciting to me because Lean is catalyzing collaboration between mathematics the same way Google Docs catalyzed collaboration between Methodists.
(Not) collaborating on mathematics
I think it’s fair to say that collaboration at the forefront of mathematics is, generally speaking, pretty difficult. Lots of the most famous modern mathematical results involve individuals or very small groups — always building on the prior work of many, many others, but often doing that building in temporary isolation. As two examples, Wiles proved Fermat’s Last Theorem (based on work a decade earlier on the Taniyama–Shimura conjecture), and Perlman proved the Poincaré conjecture (based on Hamilton’s earlier work on the Ricci flow). Mathematics, to a close-by outsider like myself, feels like a highly social activity, but it’s social the way correspondence chess is social, not the way Liverpool Rummy is social.
I don’t want to overstate my case too much: there are some modern examples of massive collaborations, like the hundred or so people who worked on the classification of finite simple groups. And there are lots of dynamic duos in mathematics. Two minds may be even better than one! There are also folks like Paul Erdős, a mathematician who famously specialized in being one half of many, many dynamic duos.
I would not consider myself someone who works at the forefront of mathematics, but in my modest mathematical research, I’ve experienced the difficulty with developing results in groups. When you’re working on an unfinished mathematical result, there are lots and lots of details, the details are connected in non-obvious ways, and needing to make a change to one part of a proof can have consequences to other parts that aren’t obvious. When it’s you and multiple other people, it can feel like most of your time is spent making sure everyone is tracking the changes to the details rather than making new progress. (I can recall one math-heavy three-author paper I was involved in that was really the result of a series of two-person collaborations. Despite significant effort, we were never able to get on the same page at the same time.)
Computer-checked proof
The idea of using computers to check mathematical proofs is not a new idea. The idea is older than I am, and by the time I entered college around the turn of the century, the question was not “is it a reasonable idea for computers to check your proofs?” but “when is it worth the effort?” In my corner of academic computer science — the study of programming languages — I’d say the answer for about a decade has been “it’s worth doing computer checked proof whenever you’re doing something moderately complicated.” (If you want to say almost anything about a real programming language that people actually use, you’re doing something moderately complicated.) The Rocq theorem prover has become the tool of choice in my little corner of computer science: so far in 2025, there are at least 22 published papers that used a specific Rocq library called Iris! Agda, Isabelle, and HOL Light are also popular options; I’ve personally done a fair amount of work in Agda.
In my experience, when you’re collaborating with other people while the computer is actively checking your work, the difficult detail-management problem changes: instead of a difficult human communication problem, managing the details becomes a (comparatively straightforward) programming problem. More than once I’ve made a change to one part of a proof, seen that it causes problems in someone else’s work, and then gone and fixed their problem without really having to understand the actual details of what they were doing.
It’s not a new observation that computer-assisted mathematics unlocks a kind of collaboration that isn’t otherwise feasible. In 1998, Thomas Hales presented a proof of the Kepler Conjecture, which says that the way you stack oranges in a grocery store is really and truly the best way to pack spheres without wasting any space. His proof was 300 pages long and had one author! It was so complex that a group of twelve reviewers spent four years trying to understand the proof, and after four years they said they still weren’t sure it was correct. The experience inspired Hales to spend the next decade creating a computer-checked version of the proof, but the second time he collaborated with twenty-one other people.
Lean!
I think it’s fair to say that the tools I just described for computer-checked proof have not quite caught on outside of computer science. I also think it’s fair to say that Lean, the system I’m working on now, has started catching on, at least with mathematicians. (I can’t confidently opine as to why that’s the case; as with most things, there’s surely a combination of good design, thoughtful community building, timing, and luck.) I want to mention three really cool ways in which people are collaborating on mathematics in Lean in new ways.
The first is a massive collaboration, Mathlib, that is currently aiming to capture a ton of reasonably well-known mathematics — including most of the math that you might learn in high school or college — in Lean. Over five hundred people have directly contributed to Mathlib, and many, many more have used it as a starting point for their work.
The second is a collaborative project to formalize Carleson’s theorem, a famously tricky result. (The Wikipedia article on it states “Carleson’s original proof is exceptionally hard to read, and although several authors have simplified the argument there are still no easy proofs of his theorem.”) The project to formalize Carleson’s theorem in Lean started with five collaborators, and the successfully completed proof lists seventeen collaborators.
The third, and my real inspiration for writing this post, is the equational theories project. If you have a mathematical statement A and another mathematical statement B, you can ask yourself the question “if I assume A, can I prove B?” You may be able to show that the answer is “yes,” you may be able to show that the answer is “no,” and you might be stuck and unable to answer either yes or no. About a year ago, the well-known mathematician Terrence Tao came up with 4694 interesting mathematical statements, which meant that there were 4694 ways to pick a mathematical statement A and then 4693 ways to pick a different statement B. That results in about twenty-two million mathematical questions. As an intentional experiment in collaborative mathematics, Tao proposed trying to answer “yes” or “no” to all of them. And it worked! More than five dozen people contributed to the project, with twenty-eight people listed as mathematical contributors, and all twenty-two million questions were verified in Lean. Most questions were very easy, and some questions took multiple months with multiple people working on one question.
Most of the people working with Hales on the formalization of the Kepler conjecture were doing it as paid work. Essentially everyone working on the equational theories project was just doing mathematics for fun in their free time, and making mathematical discoveries along the way! That feels like something new, and a little magical.
But what are you doing, Rob?
In an early draft I talked more about what I’m actually going to be working on at my new job, but Shae was a thoughtful early reader and pointed out that I’d already finished a complete thought. I’ll stop here and save other thoughts for the future. Thanks to the early readers, especially Shae, Ashley, and my parents.
If you’re interested in a tiny taste of what doing mathematics in Lean feels like, I recommend the Natural Number Game. If you’re generally interested in programming, I recommend Functional Programming in Lean, because Lean is a cool programming language in addition to being a tool for checking mathematical proofs. If you know what Zulip is, Lean has a Zulip.