[Agda] Type Theory Makes Headlines ; -) [ACM TechNews, Monday, July 1, 2013]

[Wolfram Kahl]

----- Forwarded message from ACM TechNews <technews at HQ.ACM.ORG> -----
Date: Mon, 1 Jul 2013 11:45:08 -0400
From: ACM TechNews <technews at HQ.ACM.ORG>
Subject: ACM TechNews, Monday, July 1, 2013
To: TECHNEWS at LISTSERV.ACM.ORG

[...]

Mathematicians Think Like Machines for Perfect Proofs
New Scientist (06/25/13) Jacob Aron

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.
http://www.newscientist.com/article/dn23749-mathematicians-think-like-machines-for-perfect-proofs.html#.Uc16c5xpeZQ

[...]

----- End forwarded message -----