1900 年，希尔伯特梦想给全部数学打一个完美地基：一套公理加机械的推理规则，原则上能证明每一个真命题、也永不自相矛盾。1931 年，25 岁的哥德尔把这个梦一刀劈开。
他的武器是一句「咬自己尾巴」的话：「这句话在本系统内不可被证明。」若它能被证明，它就是假的，系统证出假命题——崩了；若它不能被证明，那它说的正是真的，可系统偏偏证不出。无论哪种，系统要么不一致，要么不完备。哥德尔的天才在于用哥德尔编码把「可证明性」这个关于数学的元陈述，翻译成算术内部一个关于数字的普通命题——数学被逼着谈论它自己。
$G$ 是那个自指命题；$\ulcorner G \urcorner$ 是 $G$ 自身的哥德尔编码（把公式变成一个唯一的自然数）；$\mathrm{Prov}(n)$ 表示「编码为 $n$ 的公式在系统内可证」。这行式子读作：「$G$ 为真，当且仅当 $G$ 不可被证明。」第一不完备定理说：任何足够强（能表达算术）且一致的形式系统里，都存在这样一个既真又不可证的 $G$。第二定理更狠：这样的系统无法在自身内部证明自己的一致性。
它的美在于把说谎者悖论从毒药炼成了定理。「我在说谎」只让人陷入死循环；哥德尔把它稍稍一改——从「我是假的」改成「我不可证」——悖论就变成一把精确的手术刀，切出真理与可证性之间那道永恒的裂缝。真比可证更大：有些命题为真，却没有任何有限的证明能抵达。这不是数学的失败，而是它诚实到能说出「有些真理我够不着」的自觉。
不完备定理是形式化验证的理论天花板：没有一个自动系统能证明所有真程序性质，这正是软件验证永远需要人的洞察的原因。哥德尔编码本身则是「程序即数据」思想的鼻祖：把代码当作可被别的代码处理的数字，正是冯·诺依曼架构与元编程的灵魂。
哥德尔证明了「有些真理证不出」，图灵把同一件事翻译成了机器的语言。1936 年他设想一台极简机器：一条无限长的纸带、一个读写头、一张「看到什么就做什么」的规则表。就这么点东西，却能计算任何可被机械计算的东西——这就是图灵机，现代计算机的数学原型。
然后他问了一个致命的问题：能不能写一个程序 $H$，输入任意程序和数据，判断它会「停机」还是「永远死循环」？直觉上似乎该能。图灵证明：不可能。招数和哥德尔如出一辙——自指加反转。
假设存在判停器 $H(P, x)$，当程序 $P$ 在输入 $x$ 上停机时返回「停」，否则返回「不停」。构造一个捣蛋程序 $D$：
现在把 $D$ 喂给它自己，问 $D(D)$ 会怎样？若 $D(D)$ 停机，按定义它该死循环——矛盾；若它死循环，按定义它该停机——又矛盾。$D$ 做的恰好和 $H$ 的预言相反。所以 $H$ 根本不存在。停机问题不可判定。
停机问题的美在于它用一台想象中的机器，为「什么能算、什么永远算不出」划了一条清晰的界。这条界不依赖任何硬件——再快的量子计算机、再大的数据中心都跨不过去，因为它是逻辑的界，不是工程的界。而图灵与哥德尔的论证共享同一个骨架：制造一个「与关于自己的预言对着干」的对象——两人从两个方向挖隧道，在同一块岩石上会师。
停机问题的不可判定性像涟漪般扩散：Rice 定理说程序的一切非平凡语义性质都不可判定——所以完美的病毒查杀、死循环检测、编译器优化在理论上都不存在，工业界只能用近似与启发式。每次 IDE 提示「可能的无限循环」却不敢下定论，背后都是图灵在 1936 年立下的界碑。
图灵用「带纸带的机器」定义计算；同一年，丘奇给出了截然不同的答案——只有函数，没有别的。没有内存、没有变量赋值、没有循环语句，宇宙里只有一件事：把一个函数作用到另一个东西上。这就是 λ 演算。
惊人的是，仅凭「定义函数」和「调用函数」两个动作，就能造出数字、真假、递归、一切可计算的东西。数字 $3$ 不再是符号，而被定义成「把一个操作重复三次」的函数。计算不再是「机器在跑」，而是「表达式在化简」——像代数里把 $(a+b)^2$ 展开一样，一步步替换到不能再简为止。
λ 演算只有三条语法：变量 $x$；抽象 $\lambda x.\,M$（定义一个「输入 $x$、返回 $M$」的函数）；应用 $M\,N$（把函数 $M$ 作用到 $N$）。核心的计算规则只有一条 —— β-归约（代入）：
读作：把函数体 $M$ 里所有的 $x$ 替换成 $N$。就这一条替换规则，反复施行，就是全部的「计算」。例如 $(\lambda x.\,x{+}1)\,4 \to 4{+}1 \to 5$。Church 编码把自然数写成 $n \equiv \lambda f.\lambda x.\,f^{n}(x)$——「把 $f$ 叠用 $n$ 次」，数字就是重复的次数。
它的美是极致的极简主义：整座计算的大厦，地基上只放了「函数」这一块砖。没有状态、没有时间、没有副作用——计算被还原成纯粹的代换与等价，一件近乎柏拉图式的静态真理。更美的是它揭示了深刻的对称：数据与操作的界限消失了。数字是函数，真值是函数，连「重复」也是函数。当你意识到「一切皆函数」竟足以撑起整个可计算世界，那种震撼不亚于发现「一切皆原子」。
λ 演算是函数式编程的直系祖先：Lisp、Haskell，乃至 Python/JavaScript 里的 lambda、闭包、高阶函数、map/reduce，全是它的后裔。Curry–Howard 同构更揭示了惊人的三位一体：程序 = 证明，类型 = 命题，运行 = 化简——类型检查器于是成了定理证明器，这正是 Coq、Lean 等证明助手的根基（对应 Day 19 范畴论与类型论）。React 的纯函数组件、不可变数据流，也是 λ 演算「无副作用」哲学的回声。
1930 年代，三个人从三个方向定义了「什么叫可计算」：哥德尔的递归函数（用最原始的加减和递归搭出）、图灵的图灵机（带纸带的机器）、丘奇的λ 演算（纯函数代换）。三种设定看上去毫无关系——一个数论，一个机械，一个函数代数。
然后奇迹发生了：它们被证明完全等价。凡一种能算的，另两种也能算，一个不多一个不少。好像三支互不通信的探险队从沙漠、海洋、丛林出发，却爬上了同一座山顶。这种「殊途同归」强烈暗示：他们摸到的不是三个人造定义，而是「可计算」这个概念本身的客观轮廓。
丘奇–图灵论题断言：这个共同的类，就等于「任何算法在直觉意义上能计算」的全部。注意它是一条论题而非定理——因为「直觉上的算法」无法被形式化，你没法证明它，只能不断验证。九十年来，人们提出的每一种计算模型（寄存器机、细胞自动机、量子计算机……）都没能超出这个类。量子计算机只是更快，能算的东西一个没多。
它的美是「稳健性即真实性」的典范。当一个概念被无数种毫不相干的方式定义、结果却始终重合，数学家就有理由相信它触到了某种独立于人类约定的实在——正如 $\pi$ 从圆、从级数、从概率里反复冒出来。丘奇–图灵论题把「可计算」从工程话题提升为一条近乎物理的定律：存在一道绝对的、模型无关的计算边界，我们所有的机器都活在它同一侧。
这条论题是整个计算机科学得以成立的许可证：正因为所有合理模型等价，我们才能安心用高级语言写算法，不必担心换台机器结论就变，「算法」也才成为绝对概念。其物理版本——「任何物理过程都可被图灵机模拟」——直通量子计算、乃至「宇宙是不是一台计算机」的哲学争论（对应 Day 36、Day 53 数学哲学）。