Communications of the ACM
Our Number's p: Machines Will Do Maths We'll Never nderstand
Some mathematicians think the field of mathematics is approaching a limit that cannot yield further breakthroughs without computerized assistance.
Credit: Roya Hamburger
Some mathematicians think the field of mathematics is approaching a limit that cannot yield further breakthroughs without computerized assistance.
Although innovations such as proof assistants have helped, using a computer to prove math concepts is still so laborious most mathematicians do not bother.
One solution being pursued by Princeton University's Vladimir Voevodsky seeks to redefine math fundamentals to make math easier for computers to understand. He notes, for example, that because computers have multiple ways of defining certain mathematical objects in terms of sets, if two computer proofs use different definitions for the same thing, they will be incompatible. "The existing foundations of maths don't work very well if you want to get everything in a very precise form," Voevodsky says.
His strategy substitutes sets with types, which define mathematical objects under stricter terms in which each concept has only one definition. The approach enables mathematicians to organize their ideas with a proof assistant directly, without having to translate them later.
However, Voevodsky notes there are levels of mathematical complexity and abstraction that are far beyond mathematicians' capabilities to attain, and computers may hold the answer. This leads to speculation that computers could eventually surpass human mathematicians to the point they become unnecessary.
From New Scientist
View Full Article - May Require Free Registration
Abstracts Copyright © 2015 Information Inc., Bethesda, Maryland, USA
No entries found