6.4 未解难题与机器证明

6.4 未解难题与机器证明：双螺旋的下一段

本节摘要：未解难题是数学的氧气，千禧年七大难题是当代的悬赏榜；机器证明从四色定理的争议起步，经开普勒猜想的计算机验证，到 Lean 形式化系统重建数学文本，正在改变"置信"的生产方式。本节盘点难题清单的含义、望月新一 ABC 争议的方法论教训、机器证明的谱系，并以 AlphaProof 一类 AI 系统的最新进展收束全册：猜想到证明的双螺旋，正被人机接力续写。

悬赏榜上的七座山峰

2000 年，克雷研究所公布七个千禧年难题，每题悬赏一百万美元。二十多年过去，只攻下一座——庞加莱猜想（第 3 章讲过佩雷尔曼的里奇流收官，他拒领了奖金）。其余六座的含义值得各用一句话理解：

注意黎曼猜想的地位：数论里大量结果是"条件性定理"（若黎曼猜想成立则……），它一旦解决，整片条件性结果瞬间转正——一座桥承重确认，整条运输线通车。

# 黎曼 zeta 与素数分布的数值一瞥：素数计数函数 vs 对数积分
import math

def count_primes(n):
    sieve = [True] * (n + 1)
    sieve[0:2] = [False, False]
    for i in range(2, int(n**0.5) + 1):
        if sieve[i]:
            sieve[i*i::i] = [False] * len(sieve[i*i::i])
    return sum(sieve)

def li_approx(n):
    # 对数积分的近似：n / ln n 的一阶修正
    return n / math.log(n) * (1 + 1 / math.log(n))

for n in [10**4, 10**5, 10**6]:
    print(n, count_primes(n), int(li_approx(n)))
# 输出：素数个数与对数积分逼近，且误差远小于 n/ln n 的粗估
# 素数定理精确刻画这个逼近速度，而它的"误差项"正由黎曼猜想的零点位置控制
​

望月新一事件：当证明长到没人读得动

2012 年，望月新一公布 ABC 猜想的证明，约六百页、建立在一套全新理论（宇宙际 Teichmüller 理论）之上。十年过去，专业共同体始终未能完成有效审查——不是发现错误，而是没有人（除作者圈子）完整消化过论证。2020 年施皮策等人的质疑与望月圈子的回应至今未有公论，期刊发表与学界承认脱节。方法论教训沉甸甸：证明的社会功能是"说服同行"，当复杂度超过审查能力，证明的公共性本身成为瓶颈——这正是形式化验证登场的结构性理由。

机器证明的谱系

第一代：计算机辅助的暴力。1976 年四色定理用计算机检查了近两千个构形，引发了"proof by computer 算不算证明"的哲学争论（第 4 章开篇提过）。1998 年开普勒猜想（球最密堆积）的证明同样依赖巨量计算机检验，审稿组花了数年才宣布"我们确信到 99%"。第二代：形式化验证。Lean、Coq 等证明助手把证明写成可机器检查的形式语言——每个逻辑步骤由内核逐行核验，"置信"从同行评审的信用系统转移到代码审计。近年标志性事件：Liquid Tensor Experiment 把数学家舒尔策本人都"从没完全确信"的一个定理在 Lean 中形式化通过，他公开表示这是第一次对此结果"完全安心"。第三代：AI 发现。2024 年前后 AlphaProof 等系统把大模型的猜想生成与搜索、形式化验证组合，在国际数学奥林匹克拿到奖牌级成绩。三代的演进本质：

机器证明三代演进

形式化的成本也如实相告：一个定理形式化的工作量通常是书写的十倍以上，数学界正在用众包与 AI 辅助压缩这个系数。它改变的是检查，不是创造——提出黎曼猜想式的洞察、选择朗兰兹式的纲领，这类"元创造力"（导读里提过）目前仍专属于人类。

# 用代码体感"验证"与"发现"的分工：验证器逐条检查 一目了然
def verify_pythagorean(triples):
    # 一个"定理验证器"的微缩模型：给定勾股数列表 逐条核验
    for a, b, c in triples:
        assert a*a + b*b == c*c, f"({a},{b},{c}) 不满足定理"
    return f"全部 {len(triples)} 条通过验证"

known = [(3, 4, 5), (5, 12, 13), (8, 15, 17), (20, 21, 29)]
print(verify_pythagorean(known))

# 而"发现"是另一个问题：欧几里得式地生成新的勾股数（构造性证明）
def generate_pythagorean(m, n):
    # 参数化公式：m>n 时 a=m^2-n^2 b=2mn c=m^2+n^2 必为勾股数
    return m*m - n*n, 2*m*n, m*m + n*n

print(generate_pythagorean(4, 3))   # (7, 24, 25)
# 验证器确认已给的（机器的强项） 参数化构造创造新的（人类洞察的强项）
# 机器证明的前沿正是让机器也参与第二类工作——但它仍在验证器划定的安全区内出手
​

收束：双螺旋的下一段

回到导读的两条线。猜想这一极，人类依然独占"提出好问题"的能力——千禧年难题、朗兰兹纲领都是猜想的殿堂级作品。证明这一极，机器从工具升格为合作者：它接管检查（形式化）、接管暴力（构形枚举）、开始接管部分战术搜索（AI 定理证明）。双螺旋没有换人，只是多了一个 strand。给读者的临别建议只有一条：无论工具多强，读懂数学的最好方式仍是本册反复演练的那个动作——拿起纸笔，从一个猜想出发，亲手走一遍证明，再用代码敲一遍。这个过程本身，就是数学。

本节要点回顾

• 千禧年难题各管一个地基：黎曼猜想承重最广，数论大片条件性结果等它转正；
• 望月 ABC 事件揭示证明的公共性瓶颈：复杂度超过审查能力时，证明的社会功能失灵；
• 机器证明三代演进的共同方向：置信从社交过程转移到机器可检查过程；
• 形式化不改变创造：检查可以外包，猜想与纲领的选择仍是人类主场；
• 全册主线收束：猜想—证明双螺旋的下一段，由人机接力续写。

（全册终）