acm-header
Sign In

Communications of the ACM

ACM TechNews

Our Number's ­p: Machines Will Do Maths We'll Never ­nderstand


View as: Print Mobile App Share: Send by email Share on reddit Share on StumbleUpon Share on Hacker News Share on Tweeter Share on Facebook
Complexity.

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