Communications of the ACM
Mathematicians Think Like Machines For Perfect Proofs
A new mathematical framework forces people to think more like machines in order to check perfect proofs in collaboration with computers.
Credit: Petrovich9/Getty
A team of mathematicians led by Vladimir Voevodsky with Princeton's Institute for Advanced Study have devised a new mathematical framework that forces people to think more like machines to check perfect proofs in collaboration with computers.
The team's manual explains the use of type theory as an alternative mathematical basis. Type theory stipulates that all proofs must describe how to mathematically construct the object they concern, which is the opposite of set theory. Once mathematicians have completed this task, their proof would automatically be supported by unshakable computational checks. It is impossible to write an incorrect proof, assuming the underlying code is defect-free, along with the automated proof assistants that verify everything as the mathematician goes along.
Voevodsky's team also says it is far easier to check the code than the entire proof in most instances. Not only does the new framework make proof-checking easier, it also is a move toward computers that one day could execute mathematics by themselves, which might potentially clear a path toward more advanced forms of artificial intelligence (AI).
"My expectation is that all these separate, limited AI successes, like driving a car and playing chess, will eventually converge back, and then we're going to get computers that are really very powerful," says project collaborator Andrej Bauer.
From New Scientist
View Full Article
Abstracts Copyright © 2013 Information Inc., Bethesda, Maryland, USA
No entries found