An old dream of computer scientists is to build an optimally efficient universal problem solver. The Gödel machine of Juergen Schmidhuber (2003) solves arbitrary computational problems in an optimal fashion inspired by Kurt Gödel's celebrated self-referential formulas (1931). It starts with an axiomatic description of itself, and we may plug in as an axiom any formalizable problem description or utility function, such as the expected future reward of a robot. Using an efficient proof searcher, the Gödel machine will rewrite any part of its software (including the proof searcher) as soon as it has found a proof that this will improve its future performance, given the utility function and the typically limited computational resources. Self-rewrites are globally optimal (no local minima!) since provably none of all the alternative rewrites and proofs (those that could be found by continuing the proof search) are worth waiting for.
