Idea: the Amsterdam Theorem Exchange

In this talk, I introduce the Amsterdam Theorem Exchange: a distributed proof assistant where users on the network are able to submit formal mathematical conjectures together with a price, and – when the price is right – the system returns either with a proof or a counter-example. Also there are solvers on the network that seek valuable but outstanding mathematical problems, trying to tackle them by using human and artificial intelligence. This talk explains how and what formal methods are needed to implement this system, that subnets specialize to solve different classes of problems, and argues that the Amsterdam Theorem Exchange is more valuable than all cryptocurrency systems combined – since problems include e.g. prime factoring problems and problems of reversing cryptographic functions.