Machines that touch the foundations
Parent: famous-machines
Explicit, writable Turing machines whose halting encodes a famous mathematical statement — making Gödel and the busy-beaver tangible.
Yedidia–Aaronson (2016)They constructed explicit small machines that halt iff a statement fails:
- a ~7910-state machine (later reduced to 748 by Stefan O'Rear) that halts iff ZFC is inconsistent (it searches for a proof of
0=1in ZFC);- a few-thousand-state machine that halts iff Goldbach's conjecture is false;
- one that halts iff the Riemann hypothesis is false.
The consequences make abstraction concrete:
BB(748)is independent of ZFC. If ZFC could prove the value ofBB(748), it could decide whether the ZFC-machine halts, hence prove its own consistency — impossible by Gödel's second theorem. So there is a specific, finite number that mathematics-as-we-axiomatize-it provably cannot compute.- The busy-beaver frontier is real code. These are actual programs; past a few hundred states, "does this halt?" already outruns all of current mathematics. The uncomputability of
BBisn't a far-off abstraction — it starts at machine sizes you could print on a page.
This is the sharpest concrete face of undecidability: not "some abstract program," but this one, whose fate is Goldbach's, or ZFC's own.