Peter Scholze wants to rebuild much of modern mathematics, starting from one of its cornerstones. Now, he has received validation for a proof at the heart of his quest from an unlikely source: a computer.
Although most mathematicians doubt that machines will replace the creative aspects of their profession any time soon, some acknowledge that technology will have an increasingly important role in their research — and this particular feat could be a turning point towards its acceptance.
Scholze, a number theorist, set forth the ambitious plan — which he co-created with his collaborator Dustin Clausen from the University of Copenhagen — in a series of lectures in 2019 at the University of Bonn, Germany, where he is based. The two researchers dubbed it ‘condensed mathematics’, and they say it promises to bring new insights and connections between fields ranging from geometry to number theory.
Other researchers are paying attention: Scholze is considered one of mathematics’ brightest stars and has a track record of introducing revolutionary concepts. Emily Riehl, a mathematician at Johns Hopkins University in Baltimore, Maryland, says that if Scholze and Clausen’s vision is realized, the way mathematics is taught to graduate students in 50 years’ time could be very different than it is today. “There are a lot of areas of mathematics that I think in the future will be affected by his ideas,” she says.
Until now, much of that vision rested on a technical proof so involved that even Scholze and Clausen couldn’t be sure it was correct. But earlier this month, Scholze announced that a project to check the heart of the proof using specialized computer software had been successful.
Computer assistance
Mathematicians have long used computers to do numerical calculations or manipulate complex formulas. In some cases, they have proved major results by making computers do massive amounts of repetitive work — the most famous being a proof in the 1970s that any map can be coloured with just four different colours, and without filling any two adjacent countries with the same colour.
Number-theory prodigy among winners of most coveted prize in mathematics
But systems known as proof assistants go deeper. The user enters statements into the system to teach it the definition of a mathematical concept — an object — based on simpler objects that the machine already knows about. A statement can also just refer to known objects, and the proof assistant will answer whether the fact is ‘obviously’ true or false on the basis of its current knowledge. If the answer is not obvious, the user has to enter more details. Proof assistants thus force the user to lay out the logic of their arguments in a rigorous way, and they fill in simpler steps that human mathematicians had consciously or unconsciously skipped.
Once researchers have done the hard work of translating a set of mathematical concepts into a proof assistant, the program generates a library of computer code that can be built on by other researchers and used to define higher-level mathematical objects. In this way, proof assistants can help to verify mathematical proofs that would otherwise be time-consuming and difficult, perhaps even practically impossible, for a human to check.
Proof assistants have long had their fans, but this is the first time that they have had a major role at the cutting edge of a field, says Kevin Buzzard, a mathematician at Imperial College London who was part of a collaboration that checked Scholze and Clausen’s result. “The big remaining question was: can they handle complex mathematics?” says Buzzard. “We showed that they can.”
And it all happened much faster than anyone had imagined. Scholze laid out his challenge to proof-assistant experts in December 2020, and it was taken up by a group of volunteers led by Johan Commelin, a mathematician at the University of Freiburg in Germany. On 5 June — less than six months later — Scholze posted on Buzzard’s blog that the main part of the experiment had succeeded. “I find it absolutely insane that interactive proof assistants are now at the level that, within a very reasonable time span, they can formally verify difficult original research,” Scholze wrote.
AI maths whiz creates tough new problems for humans to solve
The crucial point of condensed mathematics, according to Scholze and Clausen, is to redefine the concept of topology, one of the cornerstones of modern maths. A lot of the objects that mathematicians study have a topology — a type of structure that determines which of the object’s parts are close together and which aren’t. Topology provides an idea of shape, but one that is more malleable than those of familiar, school-level geometry: in topology, any transformation that does not tear an object apart is admissible. For example, any triangle is topologically equivalent to any other triangle — or even to a circle — but not to a straight line.
Topology plays a crucial part not only in geometry, but also in functional analysis, the study of functions. Functions typically ‘live’ in spaces with an infinite number of dimensions (such as wavefunctions, which are foundational to quantum mechanics). It is also important for number systems called p-adic numbers, which have an exotic, ‘fractal’ topology.
A grand unification
Around 2018, Scholze and Clausen began to realize that the conventional approach to the concept of topology led to incompatibilities between these three mathematical universes — geometry, functional analysis and p-adic numbers — but that alternative foundations could bridge those gaps. Many results in each of those fields seem to have analogues in the others, even though they apparently deal with completely different concepts. But once topology is defined in the ‘correct’ way, the analogies between the theories are revealed to be instances of the same ‘condensed mathematics’, the two researchers proposed. “It is some kind of grand unification” of the three fields, Clausen says.
Scholze and Clausen say they have already found simpler, ‘condensed’ proofs of a number of profound geometry facts, and that they can now prove theorems that were previously unknown. They have not yet made these public.
There was one catch, however: to show that geometry fits into this picture, Scholze and Clausen had to prove one highly technical theorem about the set of ordinary real numbers, which has the topology of a straight line. “It’s like the foundational theorem that allows the real numbers to enter this new framework,” Commelin explains.
Clausen recalls how Scholze worked relentlessly on the proof until it was completed ‘through force of will’, producing many original ideas in the process. “It was the most amazing mathematical feat I’ve ever witnessed,” Clausen recalls. But the argument was so complex that Scholze himself worried there could be some subtle gap that invalidated the whole enterprise. “It looked convincing, but it was simply too novel,” says Clausen.
For help checking that work, Scholze turned to Buzzard, a fellow number theorist who is an expert in Lean, a proof-assistant software package. Lean was originally created by a computer scientist at Microsoft Research in Redmond, Washington, for the purpose of rigorously checking computer code for bugs.
Buzzard had been running a multi-year programme to encode the entire undergraduate maths curriculum at Imperial into Lean. He had also experimented with entering more-advanced mathematics into the system, including the concept of perfectoid spaces, which helped to earn Scholze a Fields Medal in 2018.
Commelin, who is also a number theorist, took the lead in the effort to verify Scholze and Clausen’s proof. Commelin and Scholze decided to call their Lean project the Liquid Tensor Experiment, in an homage to progressive-rock band Liquid Tension Experiment, of which both mathematicians are fans.
A febrile online collaboration ensued. A dozen or so mathematicians with experience in Lean joined in, and the researchers got help from computer scientists along the way. By early June, the team had fully translated the heart of Scholze’s proof — the part that worried him the most — into Lean. And it all checked out — the software was able to verify this part of the proof.
Better understanding
The Lean version of Scholze’s proof comprises tens of thousands of lines of code, 100 times longer than the original version, Commelin says. “If you just look at the Lean code, you will have a very hard time understanding the proof, especially the way it is now.” But the researchers say that the effort of getting the proof to work in the computer has helped them to understand it better, too.
LINK AI Copernicus ‘discovers’ that Earth orbits the Sun
Riehl is among the mathematicians who have experimented with proof assistants, and even teaches them in some of her undergraduate classes. She says that, although she doesn’t systematically use them in her research, they have begun to change the very way she thinks of the practices of constructing mathematical concepts and stating and proving theorems about them. “Previously, I thought of proving and constructing as of two different things, and now I think of them as the same.”
Many researchers say that mathematicians are unlikely to be replaced by machines any time soon. Proof assistants can’t read a maths textbook, they need continuous input from humans, and they can’t decide whether a mathematical statement is interesting or profound — only whether it is correct, Buzzard says. Still, computers might soon be able to point out consequences of the known facts that mathematicians had failed to notice, he adds.
Scholze says he was surprised by how far proof assistants could go, but that he is unsure whether they will continue to have a major role in his research. “For now, I can’t really see how they would help me in my creative work as a mathematician.”
