Mathematicians Welcome Computer-Assisted Proof in 'Grand Unification' Theory

Proof-assistant software handles an abstract concept at the cutting edge of research, revealing a bigger role for software in mathematics. From a report: 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. 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 based on 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 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."

Read more of this story at Slashdot.

from Slashdot https://ift.tt/3j4waKP

Share on FacebookPlus on Google+

SUBSCRIBE TO OUR NEWSLETTER