Posts
Davide Castelvecchi, Senior Reporter - Physical Sciences notes, Proof-assistant software handles an abstract concept at the cutting edge of research, revealing a bigger role for software in mathematics.
Efforts to verify a complex mathematical proof using computers have been successful
Photo: Fadel Senna/AFP via Getty
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...
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.
Additional resources
Nature 595, 18-19 (2021)
doi: https://doi.org/10.1038/d41586-021-01627-2
Source: Nature.com
