### 产品中心

### 主页 > >

By Jacob Aron (Image: Petrovich9/Getty) It’s difficult to get computers to think like humans, so mathematicians are trying the opposite. A proposed mathematical framework forces humans to think more like machines in order to harness the remarkable ability of computers to rapidly check proofs. The framework provides the possibility of proofs that can’t be wrong – and so wouldn’t need to be laboriously checked by humans. It could also be the first step towards computers carrying out mathematics by themselves, and perhaps even more advanced forms of artificial intelligence. Mathematical proofs are becoming so complex that even other mathematicians have a hard time following them. One solution is to use computer-verified proofs, in which software double-checks each logical step in a proof to ensure its correctness. There’s just one problem – the current foundations of mathematics, laid down around a hundred years ago, make it difficult to translate human-written proofs into ones that machines can follow. Now a team of mathematicians led by Vladimir Voevodsky of the Institute for Advanced Study in Princeton say they have a new, 21st century way to do maths, working in collaboration with computers by speaking their language. You wouldn’t necessarily know it, but all of maths is currently founded on set theory, the study of collections of objects, which helped resolve a variety of logical paradoxes encountered by mathematicians in the early 20th century. In theory any proof can be rigorously written in the language of sets, but mathematicians don’t normally bother. For example, the number zero is the empty set, which contains no objects, the number one is the set containing one empty set, the number two is the set containing the sets describing one and zero, and so on. In this example, sets provide a way for numbers to emerge from nothing. Most computer-verified proofs are not based on set theory. They favour another foundation – type theory. The difference between a set and a type is a subtle but important one. “Think of the elements of a set as grains of sand,” says Andrej Bauer of the University of Ljubljana, Slovenia, who worked on the project. “You can build a sandcastle, but you have to work hard to make it.” The elements of a type are more like different arrangements of a collection of building blocks, their structure limited by the basic shape of the blocks. “The type is the stuff we can make following the rules of construction.” Type theory is more restrictive about the elements within a given type, but less restrictive in the sense of what counts as a type. In set theory, logical statements about sets are not also sets. In type theory, statements about types are themselves types. It is this quality that makes type theory ideal for computers – and that makes it self-proving. Last week, Voevodsky and colleagues have completed a 600-page instruction manual explaining how mathematicians can use type theory as an alternative foundation of mathematics. In this new way of working, mathematicians would still publish papers written in a mix of English and equations as normal but they would have to make a philosophical shift to better gel with computers. Under set theory it is possible to prove that a mathematical object exists without fully describing it, which is not allowed under type theory – all proofs must also tell you how to mathematically build the object they concern. The reward? Once they have done this work, their proof would automatically be backed up by rock-solid computational checks – in a neat demonstration, the mathematics in the new manual was carried out in this way. Assuming the underlying code – and the automated proof assistants that verify everything as the mathematicians goes along – is bug-free, it’s impossible to write a proof that isn’t correct. And for most proofs, it’s much easier to check the code than the whole proof, Voevodsky’s team claims. Take the case of the 500-page proof of the long-standing abc conjecture published by Shinichi Mochizuki of Kyoto University in Japan last year. Nine months on, his colleagues still have no idea whether it is correct. “That is an excellent example of a proof where a serious mathematician produces something that is very hard to understand,” says Bauer. “If mathematicians always proved things with computers, there would be no question whether there is a mistake.” That change won’t happen over night, of course. “In the short to medium term almost all mathematicians will continue in their present modes of thinking,” says Peter Aczel of the University of Manchester, UK, who also worked on the project. Others are less keen on shifting to type theory right now. Joel Hamkins of the City University of New York, says proof assistants aren’t sophisticated enough yet to be worth making the change. “Any change in the foundations from set theory would simply be an irrelevant distraction,” he says. But he accepts that this is the way mathematics is heading. “In the long run, I believe that all mathematical work will be proof-checked in this way before it is widely accepted,” he says. As well as making proofs easier to check, the new framework is a step towards computers that make their own mathematical leaps. Attempts at automated ways of proving theorems have so far been limited to extremely basic problems, but closer cooperation with humans, as suggested by Voevodsky’s team, could change that. “We’ve already learned the lesson that we don’t know how to program computers so they will have original mathematical ideas, maybe some day it will happen, but right now we know how to cooperate with computers,” says Bauer. “My expectation is that all these separate, limited AI success, like driving a car and playing chess, will eventually converge back, and then we’re going to get computers that are really very powerful.” Since this article was first published on 25 June 2013,