The Gödel Machine: Self-Improvement With a Proof Attached

Long before "recursive self-improvement" became a phrase people put in grant proposals, Jürgen Schmidhuber wrote down what it would actually take — mathematically. Not a loop of self-prompting, not a fine-tuning trick, but a machine that can rewrite any part of its own code, including the part that decides how to rewrite itself, and do so with a guarantee: every self-modification is provably useful, and provably the best modification available. The catch, and the glory, is the proof.

The machine that must prove it before it improves

A Gödel machine starts life as ordinary code, p(1), with two subroutines. The first is e(1), a problem-solving policy for interacting with the environment — it can be any traditional reinforcement learning algorithm, typically a suboptimal one. The second is a general proof searcher. That pairing is the whole bet: the dumb policy acts, while the proof searcher works in the background trying to prove that some rewrite of the machine's own code would yield higher utility.

To make proofs about itself possible, the machine carries an axiomatic system, A, encoded in its initial code. The axioms describe four things: the exact semantics of the hardware (how every instruction changes machine state, so proof techniques can reason about the effects of any program, including the proof searcher itself), the initial code p(1) itself (self-reference without circularity, in the spirit of Gödel's 1931 self-referential formulas), the probabilistic behavior of the environment, and a formal utility function — typically expected cumulative future reward, explicitly accounting for the computational cost of the proof search itself.

The proof searcher systematically tests proof techniques: programs whose outputs are proofs, using an online extension of Levin's Universal Search. Each candidate is a pair (switchprog, proof), where switchprog is an arbitrary self-rewrite program and proof is a purported proof of the target theorem, which states, roughly: executing switchprog right now yields higher utility than leaving p as is. The moment such a proof is found, the machine executes switchprog — which may completely rewrite p, including the proof searcher.

Why the proof buys you global optimality

This is where the paper earns its title. Theorem 4.1, the Global Optimality Theorem, shows the self-improvement strategy is not greedy. The trick is in how "leaving p as is" is evaluated: the utility of not switching implicitly accounts for every alternative switchprog the unmodified machine might discover later, because the proof searcher is part of p. For the target theorem to be provable, the machine must essentially prove that continuing to search for a better rewrite isn't worth the compute — the cost of search is inside the utility function. So an executed rewrite isn't just better than the status quo; it's the best of all self-changes the machine could have found, relative to its resources and proof strategy.

A Gödel machine's self-rewrite is globally optimal — no local maxima — because the code first had to prove that continuing the proof search for alternative self-rewrites was itself not useful.

The initial proof searcher is additionally O()-optimal (Theorem 5.1): no proof searcher can find proofs asymptotically faster by more than a constant factor. But Schmidhuber is explicit that O()-optimality leaves enormous room on the table — all the constant factors, all the engineering. Unlike Hutter's AIXI-style approaches with hardwired searchers, a Gödel machine can rewrite its own proof searcher to capture speedups hidden by the O() notation, whenever such speedups are provable at all. The recursion goes all the way down: the optimizer optimizes the optimizer, with a certificate each time.

Why nobody built one

The paper is pure theory — there are no experiments, no benchmarks, no ablations. And the reasons are structural. First, proof search over an axiomatic system rich enough to describe hardware, environment, and utility is astronomically expensive; the O()-optimal searcher is optimal the way a snail is optimal among snails. Second, Gödel's incompleteness theorems bite: any sufficiently rich formal system contains true statements it cannot prove, so some genuinely useful self-rewrites are forever out of reach. Schmidhuber's shrug is memorable: if no proof of a rewrite's utility exists, humans can't do much about it either. Third, the whole apparatus demands a fully formalized utility function and an axiomatized environment — fine for a robot in a simulated gridworld, hopeless for the open world.

The paper knows this. Its later sections are examples, relations to prior work (Levin search, Hutter's universal AI, Lenat's Eurisko/AM), and a FAQ addressing objections — including, with a straight face, a technical justification of consciousness. It reads less like a blueprint and more like a boundary marker: this is what rigorous self-improvement would require.

Where it sits in the RSI arc

Every empirical RSI system that followed is, knowingly or not, a heuristic relaxation of the Gödel machine. AIDE^2 replaces the proof searcher with an outer-loop agent and the target theorem with held-out benchmark grades. Gödel Agent replaces proofs with "the LLM thinks this patch helps." Self-Rewarding LMs replace the formal utility with learned preferences. Each trade is the same: give up the guarantee, keep the loop, and hope the empirical signal correlates with the utility you actually wanted.

That's why this paper still belongs at the head of any RSI reading list. It defines the ceiling — self-improvement with a certificate of global optimality — and thereby names exactly what every later method sacrifices: provability, in exchange for tractability. The open question it leaves behind is whether any middle ground exists. Can we get machine-checkable certificates for some classes of self-modification — say, verified rewrites of a training loop, or proof-carrying improvements to an optimizer — without demanding a proof about the whole future? Twenty years on, that gap between "provably optimal" and "worked on the benchmark" is still where the entire field lives.

Paper: Gödel Machines: Self-Referential Universal Problem Solvers Making Provably Optimal Self-Improvements — Jürgen Schmidhuber, 2003.