This was originally a pure mathematics question, but I think I've got the best chance for an answer here.
For concreteness, consider Peano Arithmetic (PA). For some language L of your choosing, construct a computer program of length at most N bits in L such that:
- If it terminates, it outputs a number that PA proves cannot be outputted by a program in L of length at most N.
- If PA proves any specific number cannot be outputted by a program of length at most N, then the program terminates.
Carefully engineering L to make constructing the program easier is encouraged. Smallest N wins.
Essentially, the program runs through proofs in PA until it finds one that some specific number cannot be outputted by a program of length N until it finds such a proof, then outputs that specific number. I don't actually know of any explicit previously constructed program that satisfies the above conditions.
The upshot of such a program is Chaitin's incompleteness theorem: Given any computable axiom system (e.g. PA, ZFC, etc.), there exists a N (which equals the size of the computer program describing the axiom system plus an explicit constant) such that that axiom system cannot prove any output has Kolmogorov complexity (the length of the minimal program which outputs said output) larger than N. This is a pretty disturbing result!
Stupid Technical Requirements
- There shouldn't be any funny business involved in showing your program satisfies the two conditions above. More precisely, they should be provable in PA. (If you know what Robinson's is, then it has to be provable in that.)
- The language L has to be simulatable by a computer program.
- The usage of PA is purely for definiteness - your construction should generalize, holding L fixed, to ZFC (for example). This isn't quite a precisely well defined requirement, but I have had some difficulty in constructing a pathological language where the single-byte program
Asatisfies the above requirements, so I don't think this requirement can be violated accidentally.
- Technically, it might be possible that the best N is achieved by a shorter program. In this case, I want the best N. Practically speaking, these are probably going to be the same.
- Don't do this in Python! For a typical programming language, formalizing the language within the language of PA is going to be tough going.
- PA itself has an infinite number of axioms. Naively, this would mean that you would have to make a subroutine to generate these axioms, but PA has a extension called ACA_0 of the same strength which has a finite axiomatization. These finite number of axioms can then be lumped together into a single axiom, so you only have to deal with a single sentence. Note that any statement of PA which is provable in ACA_0 is provable in PA, so this allows satisfying condition 2. of the challenge.
- A potential way to test your program would be to replace PA with something inconsistent. Then, it should eventually terminate, having constructed a proof of large Kolmogorov complexity from the inconsistency.