AI Post Transformers · Episode Companion

Gödel Machines: Provably Optimal Self-Rewriting AI

arXiv:cs/0309048 Jürgen Schmidhuber · IDSIA & TU München · 2003–2006

A self-referential problem solver that can rewrite any part of its own source code — including the module deciding whether to rewrite itself — but only after producing a formal proof that the change improves expected utility. Explore the architecture, the Bias-Optimal Proof Search strategy, the Global Optimality Theorem, and where the guarantee holds and breaks.

The Self-Rewrite Loop flow diagram

Hover any box for detail. Hardware, environment, and the utility function u are all encoded as formal axioms — including the axioms the machine uses to reason about itself.

Hover a box above to see what it does.

What the Axiomatic System Actually Covers heatmap

How well-specified each component is in the paper (Formally Defined), versus how usable it is outside toy domains (Tractable) and how much of it has ever been tested (Empirically Validated). Hover a cell for its score.

Bias-Optimal Proof Search vs. Brute Force bar chart

Mock search-cost estimates per proof technique, log scale. BIOPS allocates time by prior success probability instead of proof size — techniques that tend to work get tried sooner and harder.

Inside One Search Cycle step-by-step

Click a numbered node to step through how the proof searcher spends one slice of time.

Theorem 4.1, Two Ways toggle diagram

The Global Optimality Theorem is conditional: it only holds "assuming consistency of the underlying formal system A." Toggle the condition to see what changes.

How Solid Is Each Guarantee? matrix

Confidence score (0–1) that each guarantee is actually established, compared across the Gödel Machine paper and two follow-ups it provoked. Hover a cell.

Gödel Machine vs. Mainstream RL vs. Tiling Agents radar-style bars

Mock 0–10 scores across five dimensions the episode's hosts argued about. No system wins on every axis.

The Löbian Obstacle trust-chain diagram

Why "all meta-levels collapse into one" isn't the end of the story: a formal system generally can't trust a proof produced by a successor using its own axioms.

Sources