It鈥檚 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鈥檛 be wrong 鈥� and so wouldn鈥檛 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.
Advertisement
One solution is to use computer-verified proofs, in which software double-checks each logical step in a proof to ensure its correctness. There鈥檚 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 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.
Sandcastle sets
You wouldn鈥檛 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鈥檛 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. 鈥淭hink of the elements of a set as grains of sand,鈥� says of the University of Ljubljana, Slovenia, who worked on the project. 鈥淵ou 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. 鈥淭he 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.
Instruction manual
Last week, Voevodsky and colleagues have 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鈥檚 impossible to write a proof that isn鈥檛 correct. And for most proofs, it鈥檚 much easier to check the code than the whole proof, Voevodsky鈥檚 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 .
鈥淭hat is an excellent example of a proof where a serious mathematician produces something that is very hard to understand,鈥� says Bauer. 鈥淚f mathematicians always proved things with computers, there would be no question whether there is a mistake.鈥�
That change won鈥檛 happen over night, of course. 鈥淚n the short to medium term almost all mathematicians will continue in their present modes of thinking,鈥� says of the University of Manchester, UK, who also worked on the project.
Artificial mathematicians
Others are less keen on shifting to type theory right now. of the City University of New York, says proof assistants aren鈥檛 sophisticated enough yet to be worth making the change. 鈥淎ny 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. 鈥淚n 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鈥檚 team, could change that.
鈥淲e鈥檝e already learned the lesson that we don鈥檛 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. 鈥淢y expectation is that all these separate, limited AI success, like driving a car and playing chess, will eventually converge back, and then we鈥檙e going to get computers that are really very powerful.鈥�
