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