AI Cooperation in Practice

Abstract

Problem 1: A program that proves statements about its own output Consider a program that knows its own source code (by quining) and contains a strong enough proof checker. The program's algorithm is as follows: try all proofs of length up to nmax, looking for a proof that the program itself returns 1. If such a proof is found, return 1. Otherwise do the same for 2, then 3, then return 0. The question is: what will the program return?