整数身上叠着两套结构：加法和乘法。各自都简单得要命，却几乎互不通气——知道 $a$ 与 $b$ 的素因子分解，对 $a+b$ 的分解几乎什么也说不出。数论里绝大多数硬骨头，根子都在这道裂缝上。
abc 猜想是对这道裂缝写下的最强一句话：加法和乘法不能合谋。一个数在乘法上"规整"，指它由少数几个素数的高次幂搭成——用很少的素材堆出很大的数，很奢侈。猜想说：一旦 $a+b=c$ 把三个数拴在一起，它们就不许同时这么奢侈。
根基 $\operatorname{rad}(n)$：把 $n$ 的素因子分解里所有指数抹平成 1 再相乘，例如 $\operatorname{rad}(72)=\operatorname{rad}(2^3\cdot 3^2)=6$。它只回答"哪些素数参与了"，不管参与得多深。
$\varepsilon$ 是任意小的正数，$K_\varepsilon$ 是只依赖 $\varepsilon$ 的常数。$\operatorname{rad}(abc)$ 小，正是"三个数在乘法上高度结构化"的度量。不等式于是说：$c$ 不可能显著超过它们的素材总量。例外确有——$1+8=9$ 而 $\operatorname{rad}(1\cdot8\cdot9)=6<9$——但对每个 $\varepsilon$ 只有有限多个。
它是一根横梁：立住之后，挂在上面的定理全部自动成立——费马大定理（对足够大的指数）、Roth 逼近定理、Mordell 猜想、Szpiro 猜想……一个不等式统摄半部丢番图分析。多数猜想是叶子，abc 是主干，而它的内容又朴素到能讲给中学生听。
abc 的"有效版本"会给出丢番图方程解的可计算上界——"验证到某处即可收工"，这正是计算数论长期缺的东西。它蕴含的 Szpiro 猜想直接约束椭圆曲线的判别式与导子之比，而这正是椭圆曲线密码选参数时要盘算的量。
更著名的是它引发的僵局：2012 年望月新一发布五百余页的宇宙际 Teichmüller 理论宣称证明；2018 年 Scholze 与 Stix 当面研讨后指出 Corollary 3.12 存在无法弥合的间隙，望月不接受；2021 年论文发表在他本人任主编的期刊上，至今主流未认可。这不是"对错未知"，而是共同体无法达成共识——数学里罕见的故障模式。
论文里的证明是写给人看的说服文本：作者赌读者会在"显然"处点头。形式化证明写给一台只认公理和推理规则的机器，每一步都必须机械可核验，没有"显然"这个词。前者像散文，后者像能编译通过的程序。
关键设计叫可信内核：无论自动化多复杂、AI 搜索多聪明，最终都得吐出一份证明项，交给一个只有几千行、被反复审读过的小内核逐条检查。于是你不需要信任 AI，只需要信任那个小盒子。
底座是 Curry–Howard 对应：
读法：命题 $P$ 同时是一个类型，证明 $p$ 同时是一个具有该类型的程序项；"$P$ 可证"等价于"类型 $P$ 非空"。这一步翻译的收益是决定性的：「检查证明对不对」退化成了「类型检查」——计算机极其擅长、且能做到确定性正确的事。
它把"数学真理"从社会共识里剥出了一个可机械核验的硬核，同时反向量出人类证明省略了多少：形式化文本与原文长度之比称为 de Bruijn 因子，早年高达数十，如今在成熟领域已降到个位数。这个数字下降的过程，就是机器一点点学会人类"心照不宣"的过程——一个可被测量的哲学问题，非常罕见。
1976 年四色定理靠机器穷举 1936 个构型，引发"这还算证明吗"的争论；Hales 的 Kepler 球堆积证明评审四年后，审稿人只敢说"99% 确信"，他随后花十一年做完全形式化（Flyspeck，2014 完工）。转折点是 2021 年 Scholze 的 Liquid Tensor Experiment：他对自己新证明中最关键一步没有把握，交给 Lean 社群，半年内验证通过——形式化第一次用于前沿研究的实时质检。
工业侧同源：CompCert 编译器、seL4 微内核的正确性都是机器检验的定理。AI 侧，Lean 提供了强化学习罕见的无幻觉奖励信号——证明要么通过要么不通过。
你算出一个数：$1.20205690315959\ldots$，不知道它是什么。扔进一台"整数关系"机器，机器说：它极可能是 $\zeta(3)$。你没有证明任何东西，但你现在知道该去证明什么了。
这正是物理学家的工作方式，而数学在二十世纪的公理化叙事里把它藏了起来。欧拉先把 $\zeta(2)$ 算到多位、认出 $\pi^2/6$，然后才去找证明。实验数学只是把发现的逻辑重新合法化，它从不冒充辩护的逻辑。
核心工具是整数关系检测：给定实数 $x_1,\dots,x_n$（算到几百位精度），寻找不全为零的整数 $a_1,\dots,a_n$ 使
PSLQ 与 LLL 算法能在多项式时间内找出这样的关系（若存在且精度够）。用法很直接：让 $x_k$ 取待测常数的各次幂或若干已知常数，一旦机器吐出整数系数，就等于猜出了一个封闭形式。精度是这里的显微镜：位数不够，真关系看不见；位数够多，假关系被排除到近乎不可能。
最漂亮的战果是 1995 年的 BBP 公式，它是被 PSLQ 搜出来的，事后才证明：
关键是那个 $16^{-k}$：它让人能直接算出 $\pi$ 的第 $n$ 位十六进制数字，而不必算出前面所有位。两千年里没人想过这有可能——因为没人有理由去想。发现它的不是洞察，是搜索：搜索也能撞出人类想象力之外的结构。
OEIS（整数数列在线大典）每天在做同一件事：扔进一串数字，认出它背后的组合对象。理论物理里 Feynman 积分的封闭形式常靠数值识别猜出（多重 zeta 值），再回头严格推导。2021 年 DeepMind 与牛津、悉尼的数学家用神经网络在纽结不变量的大规模数据上找显著依赖，据此提出并由人类证明了一个新定理——机器不是证明者，而是猜想生成器：它在高维数据里指方向，人给出理由。
我们习惯把"证明"当成客观对象。但真实运作中，一个证明被接受，是因为足够多有能力的人读懂了并且信了——这是社会过程。三种压力正同时挤压它：证明太长（有限单群分类横跨数百篇论文近万页，部分作者已去世）；太机器（四色、Kepler 的穷举无人能通读）；太个人（IUT 至今只有极少数人声称理解）。
把三件常被混为一谈的事分开来看：
哥德尔完备性定理给出：一阶逻辑内 $\vdash\varphi$ 与 $\models\varphi$ 等价。但 $\mathsf{Acc}$ 从不等于 $\vdash$——没有一篇真实论文是写成形式推导的。全部数学实践都活在这道缝里。
承认这道缝并不削弱数学，反而解释了它的效率：省略正是人类数学可读的原因——完全形式化的文本正确得无懈可击，也几乎不可能读懂。数学其实同时追两个目标：确证与理解。它们长期被同一个动作（写证明）顺带完成，于是没人注意到那是两件事。机器第一次把它们拆开了——这才是"边疆"真正的位置。
形态已经出现。AlphaGeometry 与 AlphaProof 在 IMO 题目上达到银牌水平，其可靠性来自 Lean 的机械核验而非模型的自信。陶哲轩主持的 Equational Theories Project 用"Lean + 众包 + AI"在数周内判定了两千余万个蕴含关系——这个规模的协作在纸笔时代根本不构成可行的组织形式。陶称之为"工业级数学"：人提问、拆解、把握品味，机器穷举与核验。