Proof Assistant Makes Jump to Big-League Math

Computer proof assistants have been an intriguing subplot in mathematics for years — promising to automate core aspects of the way mathematicians work, but in practice having little effect on the field.

But a new result, completed in early June, has the feel of a rookie’s first hit in the big leagues: At last, a proof assistant has made a real contribution to the leading edge of mathematical research by verifying the correctness of a complicated, modern proof.

“It demonstrates that modern maths can be formalized in a theorem prover,” said Bhavik Mehta, a graduate student at the University of Cambridge who contributed to the work.

The proof in question is by Peter Scholze of the University of Bonn, one of the most widely respected mathematicians in the world. It is just one piece of a larger project called “condensed mathematics” that he and Dustin Clausen of the University of Copenhagen have been working on for several years.

Their goal is to create new foundations for topology, replacing the traditional notion of a topological space — whose examples include the sphere and the doughnut — with more versatile objects that the authors call condensed sets. In this new perspective, topological spaces are thought of as being assembled from infinite points of dust glued together.

That project includes a particularly important, difficult proof that Scholze worked out himself during a consuming week in July 2019. It establishes that an area of math called real functional analysis still works if you replace topological spaces with condensed sets.

Scholze began the proof on a Monday. He worked entirely in his head, barely writing anything down, let alone using a computer. By Thursday afternoon he’d nearly figured it out, save one piece that he just couldn’t get right. He was also feeling the strain of the intense concentration required to hold such a complicated argument in his active memory. So that night he unwound with some friends at a bar. He paid for it the next morning, Friday.

“I was completely hungover,” said Scholze.

But he also knew that he wouldn’t have time to work over the weekend, making Friday his best chance to finish the proof. The thought of losing touch with everything he’d built up in his mind over the past week, then having to start again fresh on Monday, was more than he wanted to consider.

“I didn’t think I’d have the mental capacity to rebuild this in my head again,” said Scholze.

So he powered through and finished the proof. But afterward, he wasn’t certain that what he had done was correct. The reason was more than the hazy circumstances in which he’d cleared the final hurdle. The proof was so complicated Scholze knew it was possible he had missed something.

“It’s some very convoluted thing with many moving parts. It’s hard to know which parts move by how much when you shift one of these parameters,” said Scholze.

Scholze didn’t find time to actually write down the proof until November 2019. A year later he contacted Kevin Buzzard, a mathematician at Imperial College London and a prominent evangelist for a proof assistant program called Lean. Scholze wanted to know whether it would be possible to type his proof into Lean — turning it into lines of code like a software program — so that the program could verify whether it was really true.

Buzzard shared Scholze’s inquiry with a handful of other members of the Lean community including Johan Commelin, a postdoctoral researcher at the University of Freiburg. Commelin had the perfect background for the job — he’d been using Lean for several years and was familiar with condensed mathematics — and he was convinced that verifying Scholze’s proof would do a lot to legitimize the proof assistant’s standing in the mathematical community.

“Being able to collaborate with Peter on such a project and having his name attached to it would be an enormous boost for Lean,” said Commelin.

But he also thought it could take a year or more to do it, which gave him pause. Commelin was worried he might spend all that time verifying the proof and, at the end, the rest of the math world would just shrug.

“I thought that if I spend two years working on this and I come out of my cave and say, ‘This is fine,’ the rest of the world is going to say, ‘Wow, we already knew this, Peter proved it,’” said Commelin. It wouldn’t matter that Scholze himself wasn’t entirely sure.

So Commelin asked Scholze if he’d be willing to make a public statement vouching for the importance of the work. Scholze agreed, and on Dec. 5, 2020, he wrote a post on Buzzard’s blog.

They called it the “Liquid Tensor Experiment,” a nod to mathematical objects involved in the proof called liquid real vector spaces, and to a progressive rock band he and Commelin enjoy called Liquid Tension Experiment. In the 4,400-word primer, Scholze explained some technical aspects of the result and then added a note testifying in plain language to what he saw as the importance of checking it with a computer.

“I think this may be my most important theorem to date. (It does not really have any applications so far, but I’m sure this will change,)” Scholze wrote. “Better be sure it’s correct…”

Assurance in place, Commelin set to work. After explaining to Lean the mathematical statement whose proof he ultimately wanted the program to check, he brought more mathematicians into the project. They identified a few lemmas — intermediate steps in the proof — that seemed most approachable. They formalized those first, coding them on top of the library of mathematical knowledge that Lean draws on to determine if a given statement is true or not.

Last October, Quanta wrote that the collective effort to write mathematics in Lean has the “air of a barn raising.” This project was no different. Commelin would identify discrete parts of the proof and post them to Zulip, a discussion board that serves as a hub for the Lean community. When mathematicians saw a part of the proof that fit their expertise, they’d volunteer to formalize it.

Mehta was one of about a dozen mathematicians who contributed to the work. In May he saw a post from Commelin asking for help formalizing the proof of a statement called Gordan’s lemma, which related to Mehta’s work in the area of combinatorial geometry. He spent a week coding the proof in terms that were consistent with the larger proof the mathematicians were building. It was emblematic, he said, of the way Lean works.

“It’s one big collaboration with a lot of people doing what they’re good at to make a singular monolith,” he said.

As the work proceeded, Scholze was a consistent presence on Zulip, answering questions and explaining points of the proof — a bit like an architect giving directions to builders on a job site. “He was always within reach,” Commelin said.

At the end of May the group finished formalizing the one part of the proof Scholze was most unsure about. Commelin entered the final keystroke at 1:10 a.m. on May 29. Lean compiled the proof, and it ran like a functioning program, verifying that Scholze’s work was 100% correct. Now Scholze and other mathematicians can apply those techniques from real functional analysis to condensed sets, knowing that they’ll definitely work in this new setting.

And while Scholze still prefers to work out proofs in his head, Lean’s abilities left him impressed. He can now foresee programs like it playing an enduring role in research mathematics.

“This experiment has changed drastically my impression of how capable [proof assistants] are,” Scholze said. “I now think it’s sensible in principle to formalize whatever you want in Lean. There’s no real obstruction.”