触及数学根基的机器
明确可写出的图灵机，其停机与否编码着一个著名的数学命题——让哥德尔与busy-beaver变得可以触摸。
Yedidia–Aaronson（2016）他们构造出显式的小型机器，当且仅当某个命题为假时才会停机：
- 一台约 7910 状态的机器（后来被 Stefan O'Rear 缩减到 748 状态），当且仅当 ZFC 不一致时停机（它在 ZFC 中搜索
0=1的证明）；- 一台几千状态的机器，当哥德巴赫猜想为假时停机；
- 一台当黎曼猜想为假时停机的机器。
这些结果让抽象变得具体：
BB(748)独立于 ZFC。 如果 ZFC 能够证明BB(748)的值，它就能判定那台 ZFC 机器是否停机，从而证明自身的一致性——而这由哥德尔第二定理保证是不可能的。所以存在一个具体、有限的数，是我们公理化之后的数学可证明地无法计算的。- busy-beaver 的前沿就是真实代码。 这些都是实际的程序；一旦状态数超过几百，"它会不会停机"这个问题就已经超出了当前全部数学的能力。
BB的不可计算性不是什么遥远的抽象——它从一页纸就能打印下的机器规模开始。
这是不可判定性最锋利的具体面孔：不是"某个抽象的程序"，而是这一个——它的命运，就是哥德巴赫猜想的命运，或者 ZFC 自身的命运。