“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.”