Switch to Type Theory Would Facilitate Proof Checking

A team of mathematicians led by the Institute for Advanced Study's Vladimir Voevodsky has completed a 600-page instruction manual explaining how to ground mathematics in type theory rather than set theory. 

Proofs based on type theory are more amenable than traditional ones to verification by computer, which, as proofs become ever longer and more complex, promises to be a real timesaver. 

There is also speculation among mathematicians involved in the project that their work could be the first step toward enabling computers to do mathematics by themselves.

Read New Scientist's coverage.