Building the Mathematical Library of the Future

Every day, dozens of like-minded mathematicians gather on an online forum called Zulip to build what they believe is the future of their field.

They’re all devotees of a software program called Lean. It’s a “proof assistant” that, in principle, can help mathematicians write proofs. But before Lean can do that, mathematicians themselves have to manually input mathematics into the program, translating thousands of years of accumulated knowledge into a form Lean can understand.

To many of the people involved, the virtues of the effort are nearly self-evident.

“It’s just fundamentally obvious that when you digitize something you can use it in new ways,” said Kevin Buzzard of Imperial College London. “We’re going to digitize mathematics and it’s going to make it better.”

Digitizing mathematics is a longtime dream. The expected benefits range from the mundane — computers grading students’ homework — to the transcendent: using artificial intelligence to discover new mathematics and find new solutions to old problems. Mathematicians expect that proof assistants could also review journal submissions, finding errors that human reviewers occasionally miss, and handle the tedious technical work that goes into filling in all the details of a proof.

But first, the mathematicians who gather on Zulip must furnish Lean with what amounts to a library of undergraduate math knowledge, and they’re only about halfway there. Lean won’t be solving open problems anytime soon, but the people working on it are almost certain that in a few years the program will at least be able to understand the questions on a senior-year final exam.

And after that, who knows? The mathematicians participating in these efforts don’t fully anticipate what digital mathematics will be good for.

“We don’t really know where we’re headed,” said Sébastien Gouëzel of the University of Rennes.

You Plan, Lean Chops

Over the summer, a group of experienced Lean users ran an online workshop called “Lean for the Curious Mathematician.” In the first session, Scott Morrison of the University of Sydney demonstrated how to write a proof in the program.

He began by typing the statement he wanted to prove in syntax Lean understands. In plain English, it translates to “There are infinitely many prime numbers.” There are several ways to prove this statement, but Morrison wanted to use a slight modification of the first one ever discovered, Euclid’s proof from 300 BCE, which involves multiplying all known primes together and adding 1 to find a new prime (either the product itself or one of its divisors will be prime). Morrison’s choice reflected something basic about using Lean: The user has to come up with the big idea of the proof on their own.

“You’re responsible for the first suggestion,” Morrison said in a later interview.

After typing the statement and selecting a strategy, Morrison spent a few minutes laying out the structure of the proof: He defined a series of intermediate steps, each of which was relatively simple to prove on its own. While Lean can’t come up with the overall strategy of a proof, it can often help execute smaller, concrete steps. In breaking the proof into manageable sub-tasks, Morrison was a bit like a chef instructing line cooks to chop an onion and simmer a stew. “It’s at this point that you hope Lean takes over and starts being helpful,” Morrison said.

Lean performs these intermediate tasks by using automated processes called “tactics.” Think of them as short algorithms tailored to perform a very specific job.

As he worked through his proof, Morrison ran a tactic called “library search.” It trawled Lean’s database of mathematical results and returned some theorems that it thought could fill in the details of a particular section of the proof. Other tactics perform different mathematical chores. One, called “linarith,” can take a set of inequalities among, say, two real numbers, and confirm for you that a new inequality involving a third number is true: If a is 2 and b is greater than a, then 3a + 4b is greater than 12. Another does most of the work of applying basic algebraic rules like associativity.

“Two years ago you would have had to [apply the associative property] yourself in Lean,” said Amelia Livingston, an undergraduate math major at Imperial College London who is learning Lean from Buzzard. “Then [someone] wrote a tactic that can do it all for you. Every time I use it, I get very happy.”

Altogether, it took Morrison 20 minutes to complete Euclid’s proof. In some places he filled in the details himself; in others he used tactics to do it for him. At each step, Lean checked to make sure his work was consistent with the program’s underlying logical rules, which are written in a formal language called dependent type theory.

“It’s like a sudoku app. If you make a move that’s not valid, it will go buzz,” Buzzard said. At the end, Lean certified that Morrison’s proof worked.

The exercise was exciting in the way it always is when technology steps in to do something you used to do yourself. But Euclid’s proof has been around for more than 2,000 years. The kinds of problems mathematicians care about today are so complicated that Lean can’t even understand the questions yet, let alone support the process of answering them.

“It will likely be decades before this is a research tool,” said Heather Macbeth of Fordham University, a fellow Lean user.

So before mathematicians can work with Lean on the problems they really care about, they have to equip the program with more mathematics. That’s actually a relatively straightforward task.

“Lean being able to understand something is pretty much just a matter of human beings having [translated math textbooks] into the form Lean can understand,” Morrison said.

Unfortunately, straightforward doesn’t mean easy, especially considering that for a lot of mathematics, textbooks don’t really exist.

Scattered Knowledge

If you didn’t study higher math, the subject probably seems exact and well-documented: Algebra I leads into algebra II, pre-calculus leads into calculus, and it’s all laid out right there in the textbooks, answer key in the back.

But high school and college math — even a lot of graduate school math — is a vanishingly small part of the overall knowledge. The vast majority of it is much less organized.

There are huge, important areas of math that have never been fully written down. They’re stored in the minds of a small circle of people who learned their subfield of math from people who learned it from the person who invented it — which is to say, it exists nearly as folklore.

There are other areas where the foundational material has been written down, but it’s so long and complicated that no one has been able to check that it’s fully correct. Instead, mathematicians simply have faith.

“We rely on the reputation of the author. We know he’s a genius and a careful guy, so it must be correct,” said Patrick Massot of Paris-Saclay University.

This is one reason why proof assistants are so appealing. Translating mathematics into a language a computer can understand forces mathematicians to finally catalog their knowledge and precisely define objects.

Assia Mahboubi of the French national research institute Inria recalls the first time she realized the potential of such an orderly digital library: “It was fascinating for me that one could capture, in theory, the whole mathematical literature by the sheer language of logic and store a corpus of math in a computer and check it and browse it using these pieces of software.”

Lean isn’t the first program with this potential. The first, called Automath, came out in the 1960s, and Coq, one of the most widely used proof assistants today, came out in 1989. Coq users have formalized a lot of mathematics in its language, but that work has been decentralized and unorganized. Mathematicians worked on projects that interested them and only defined the mathematical objects needed to carry their projects out, often describing those objects in unique ways. As a result, the Coq libraries feel jumbled, like an unplanned city.

“Coq is an old man now, and it has a lot of scars,” said Mahboubi, who has worked with the program extensively. “It’s been collaboratively maintained by many people over time, and it has known defects due to its long history.”

In 2013, a Microsoft researcher named Leonardo de Moura launched Lean. The name reflects de Moura’s desire to create a program with an efficient, uncluttered design. He intended the program to be a tool for checking the accuracy of software code, not mathematics. But checking the correctness of software, it turns out, is a lot like verifying a proof.

“We built Lean because we care about software development, and there is this analogy between building math and building software,” said de Moura.

When Lean came out, there were plenty of other proof assistants available, including Coq, which is the most similar to Lean — the logical foundations of both programs are based on dependent type theory. But Lean represented a chance to start fresh.

Mathematicians gravitated to it quickly. They were such enthusiastic adopters of the program that they started to consume de Moura’s time with their math-specific development questions. “He got a bit sick of having to manage the mathematicians and said, ‘How about you guys make a separate repository?’” said Morrison.

Mathematicians created that library in 2017. They called it mathlib and eagerly began to fill it with the world’s mathematical knowledge, making it a kind of 21st-century Library of Alexandria. Mathematicians created and uploaded pieces of digitized mathematics, gradually building a catalog for Lean to draw on. And because mathlib was new, they could learn from the limitations of older systems like Coq and pay extra attention to how they organized the material.

“There’s a real effort to make a monolithic library of math in which all the pieces work with all the other pieces,” said Macbeth.

The Mathlib of Alexandria

The front page of mathlib features a real-time dashboard that charts the project’s progress. It has a leaderboard of top contributors, ranked by the number of lines of code they’ve created. There’s also a running tally of the total amount of mathematics that has been digitized: As of early October, mathlib contained 18,416 definitions and 38,315 theorems.

These are the ingredients that mathematicians can mix together in Lean to make mathematics. Right now, despite those numbers, it’s a limited pantry. It contains almost nothing from complex analysis or differential equations — two basic elements of many fields of higher math — and it doesn’t know enough to even state any of the Millennium Prize problems, the Clay Mathematics Institute’s list of the most important problems in mathematics.

But mathlib is slowly filling out. The work has the air of a barn raising. On Zulip, mathematicians identify definitions that need to be created, volunteer to write them and quickly provide feedback on each other’s work.

“Any research mathematician can look at mathlib and see 40 things it’s missing,” Macbeth said. “So you decide to fill in one of those holes. It really is instant gratification. Someone else reads it and comments on it within 24 hours.”

Many of the additions are small, as Sophie Morel of the École Normale Supérieure in Lyon discovered during the “Lean for the Curious Mathematician” workshop this summer. The conference organizers gave the participants relatively simple mathematical statements to prove in Lean as practice. While working on one of them, Morel realized her proof called for a lemma — a type of short steppingstone result — that mathlib didn’t have.

“It was a very small thing about linear algebra that somehow wasn’t yet there. The people who write mathlib try to be thorough, but you can never think of everything,” said Morel, who coded the three-line lemma herself.

Other contributions are more momentous. For the last year, Gouëzel has been working on a definition of “smooth manifold” for mathlib. Smooth manifolds are spaces — like lines, circles and the surface of a ball — that play a fundamental role in the study of geometry and topology. They also often feature in big results in areas like number theory and analysis. You couldn’t hope to do most forms of mathematical research without defining one.

But smooth manifolds come in different guises, depending on the context. They can be finite-dimensional or infinite-dimensional, have “boundary” or not have boundary, and be defined over a variety of number systems, such as the real, complex or p-adic numbers. Defining a smooth manifold is almost like trying to define love: You know it when you see it, but any strict definition is likely to exclude some obvious instances of the phenomenon.

“For a basic definition, you don’t have any choice [for how you define it],” Gouëzel said. “But with more complicated objects, there are maybe 10 or 20 different ways to formalize it.”

Gouëzel had to maintain a balancing act between specificity and generality. “My rule was, I know 15 applications of manifolds that I wanted to be able to state,” he said. “But I didn’t want the definition to be too general, because then you cannot work with it.”

The definition he came up with fills 1,600 lines of code, making it pretty long for a mathlib definition, but maybe slight compared to the mathematical possibilities it unlocks in Lean.

“Now that we have the language, we can start proving theorems,” he said.

Finding the right definition for an object, at the right level of generality, is a major preoccupation of the mathematicians building mathlib. Its creators hope to define objects in a way that’s useful now but flexible enough to accommodate the unanticipated uses mathematicians might have for these objects.

“There’s an emphasis on everything being useful far into the future,” Macbeth said.

Practice Makes Perfectoid

But Lean isn’t just useful — it offers mathematicians the chance to engage with their work in a new way. Macbeth still remembers the first time she tried a proof assistant. It was 2019 and the program was Coq (though she uses Lean now). She couldn’t put it down.

“In one crazy weekend I spent 12 hours a day [on it],” she said. “It was totally addictive.”

Other mathematicians talk about the experience the same way. They say working in Lean feels like playing a video game — complete with the same reward-based neurochemical rush that makes it hard to put the controller down. “You can do 14 hours a day in it and not get tired and feel kind of high the whole day,” Livingston said. “You’re constantly getting positive reinforcement.”

Still, the Lean community recognizes that for many mathematicians, there just aren’t enough levels to play.

“If you were to quantify how much of mathematics is formalized, I’d say it’s way less than one-thousandth of one percent,” said Christian Szegedy, an engineer at Google who is working on artificial intelligence systems that he hopes will be able to read and formalize math textbooks automatically.

But mathematicians are increasing the percentage. While today mathlib contains most of the content through second-year undergraduate math, contributors hope to add the rest of the curriculum within a few years — a significant milestone.

“In the 50 years these systems had existed, not one person had said, ‘Let’s sit down and organize a coherent body of mathematics that represents an undergraduate education,’” Buzzard said. “We’re making something that will understand the questions in an undergraduate final exam, and that has never been done before.”

It will probably take decades before mathlib has the content of an actual research library, but Lean users have shown that such a comprehensive catalog is at least possible — that getting there is merely a matter of programming in all the math.

To that end, last year Buzzard, Massot, and Johan Commelin of the University of Freiburg in Germany undertook an ambitious proof-of-concept project. They temporarily put aside the gradual accumulation of undergraduate math and skipped ahead to the vanguard of the field. The goal was to define one of the great innovations of 21st-century mathematics — an object called a perfectoid space that was developed over the last decade by Peter Scholze of the University of Bonn. In 2018, the work earned Scholze the Fields Medal, math’s highest honor.

Buzzard, Massot and Commelin hoped to demonstrate that, at least in principle, Lean can handle the kind of mathematics that mathematicians really care about. “They’re taking something very sophisticated and recent, and showing it’s possible to work on these objects with a proof assistant,” Mahboubi said.

To define a perfectoid space, the three mathematicians had to combine more than 3,000 definitions of other mathematical objects and 30,000 connections between them. The definitions sprawled across many areas of math, from algebra to topology to geometry. The way they came together in the definition of a single object is a vivid illustration of the way math grows more complex over time — and of why it’s so important to lay the foundations of mathlib correctly.

“Many fields of advanced math require every kind of math you learn as an undergraduate,” Macbeth said.

The trio succeeded in defining a perfectoid space, but for now at least, mathematicians can’t do much with it. Lean needs access to much more mathematics before it can even formulate the kinds of sophisticated questions in which perfectoid spaces emerge.

“It’s a bit ridiculous that Lean knows what a perfectoid space is, but doesn’t know complex analysis,” Massot said.

Buzzard agrees, calling the formalization of perfectoid spaces a “gimmick” — the kind of early stunt that new technologies sometimes perform to demonstrate their worth. In this case, it worked.

“You shouldn’t think that because of our work every mathematician around the Earth started to use a proof assistant,” Massot said, “but I think quite a few of them noticed and asked a lot of questions.”

It will still be a long time before Lean is a real part of mathematical research. But that doesn’t mean the program is a science fiction sideshow today. The mathematicians busy developing it see their work as akin to laying the first railroad tracks — a necessary start to an important endeavor, even if they might never get to take a ride themselves.

“It will be so cool that it’s worth a big time investment now,” Macbeth said. “I’m investing time now so that somebody in the future can have that amazing experience.”

Correction: October 2, 2020

A previous version of this article misstated Patrick Massot’s university affiliation, due to a recent change in its name. The article has been revised accordingly.

This article was reprinted on Wired.com.