Getting computers to think like humans is tough but what about the opposite? A new mathematical framework gets humans to think like machines in order to harness the power of automated proof-checking. The framework provides the possibility of proofs that can't be wrong and so wouldn't need to be laboriously checked by people. It could also be the first step towards computers making their own mathematical leaps.
展开▼
