孙宇晨奖是什么？从 AI 解题到机器验证，读懂数学证明的门槛

孙宇晨奖（The Justin Sun Prize）是由孙宇晨个人出资、围绕数学题单设立的奖励计划，同时奖励解题和 Lean 形式化贡献。它把一个很具体的问题摆到了台前：AI 写出一段看似漂亮的推导，怎样才能变成别人能够检查的数学成果？这篇文章就从一道简单的整数题说起。

按截至 2026 年 9 月 17 日核对的官网 v1.0 规则，解题者获得该题分配奖金的 70%，完成 Lean 形式化并提交通过验证的 PR 的贡献者获得 30%；同一主体完成两项工作，可以获得全部分配奖金。PR 是向代码仓库提交修改、请求审核合并的一种方式。这份 70% / 30% 的分工，正好能帮助我们理解：找到证明和把证明写给机器检查，各自在做什么。

算对几个答案，距离证明还有多远？

先看一个不需要高等数学的例子：对任意整数 n，n²+n 都是偶数吗？

代入 1、2、3、4，会得到 2、6、12、20，确实都是偶数。让程序继续计算一百万个整数，可以得到更多例子，却仍没有单凭这些试算覆盖所有整数。看到这里，很容易觉得“这不就稳了吗？”可整数有无限多个，前面都算对了，还不能保证后面永远没有反例。

真正的证明可以很短：把 n²+n 写成 n(n+1)。n 和 n+1 是相邻的两个整数，其中必有一个是偶数，因此乘积能够被 2 整除。这里提供了一条适用于任意整数的理由，不必逐个代入。

如果目标范围本来就是一个明确的有限集合，完整枚举也可以成为证明的一部分，前提是确实覆盖全部情况且计算过程可靠。问题不在于能不能使用计算，而在于计算覆盖的范围，是否与命题承诺的范围一致。

同样地，AI 可以提出猜想、寻找反例或尝试推导，但这些输出需要分别判断。一个正确答案只回答了某个实例；一段证明则要交代，结论为什么在给定条件下成立。某一步套用了不满足条件的定理，后面的文字再流畅，也补不上这个缺口。

Lean 怎样检查一份证明？

Lean 是一种开源编程语言和证明助手。它允许使用者精确地写出数学对象、命题和证明，再由内核检查证明是否符合系统的推理规则。聊天模型会生成解释，Lean 内核则按形式规则核对证明对象。公式写得再像模像样，也得把推理这笔账对上。

把刚才的小例子交给证明助手，需要明确 n 是整数，偶数意味着能够写成某个整数的两倍，并把因式分解、奇偶分类和结论连接起来。实际形式化时，可以调用数学库里已有的定义和定理，也可以使用自动化工具完成部分推导，不必手工展开每一个最基础的步骤。

可以把整个过程理解为几项互相衔接的工作：

工作环节	需要完成什么
探索思路	尝试例子、寻找反例、提出可能使用的定理。
组织证明	说明前提怎样支持结论，补齐关键推导。
写成形式化表达	将对象、条件和证明转换为 Lean 能处理的内容。
检查并复核	检查形式化推导，同时核对它表达的是否仍是原来的问题。

这些环节可以反复进行。形式化过程中发现缺少一个条件，可能需要回头修改证明；探索时找到反例，也可能直接改变研究方向。人和 AI 都可以参与多个环节。Lean 则提供一个按规则检查形式化证明的环境，帮助把“提出答案”与“检查答案”分开。

为什么把证明写给机器看，也值得单独奖励？

读论文时，研究者可以凭背景知识理解“类似可得”“显然成立”或某个被省略的推导。到了形式化环境里，这些地方需要有明确的依据，或者由可检查的自动化过程补上。形式化者要理解原证明，也要知道怎样调用已有结果、怎样组织新的定义和中间结论。

例如，某一步要对一个数做除法，就需要处理分母为零的情况；某个定理只对有限集合成立，就需要确认正在使用的对象满足这个前提。这些细节并不说明原证明一定有错，却会影响它能否被完整地表达和复核。

已有数学库能减少重复工作。Lean 生态中的 Mathlib 汇集了形式化的定义和定理，可以作为后续证明的基础。但找到适用的定理、确认条件吻合，以及让论文中的表述与库中的定义对应起来，仍然需要数学理解与工程工作。

孙哥这笔悬赏里，值得留意的就是这份分工：30% 的分配奖金留给 Lean 形式化贡献者。这些补条件、找定理、对齐定义的工作，也有对应的奖励。这里的“形式化贡献者”是完成形式化并按要求提交成果的人，不应与主办方负责审核材料的人员混为一谈。擅长提出证明的人与擅长形式化的人，也因此可以围绕同一道题协作。

这项安排值得观察的地方，是它能否持续产出可复核、可复用的数学内容。如果一份成果同时补齐了后续研究需要的定义和引理，其价值可能延伸到原题之外。不过，这是对机制潜力的判断，实际效果仍要看后续提交与成果积累。

机器通过了，为什么还不能直接说“难题解决了”？

首先要看机器检查的究竟是什么。假设原题要求证明“对任意整数 n，n²+n 都是偶数”，提交者却额外加入“n 是偶数”这个前提，那么证明即使成立，也只覆盖了一部分情形。形式化检查不会替我们决定，这个更窄的命题是否足以回答原问题。

这也是为什么要区分三个层次：

• 推导成立：在写明的定义、前提和所依赖的公理下，证明能够通过检查。
• 对应原题：形式化表达保留了原问题的对象、条件与结论，没有遗漏或缩小要处理的范围。
• 符合奖项条件：成果满足该奖项对提交、资格、贡献归属及评审的要求。

形式化证明也需要检查依赖。Lean 支持在明确的逻辑基础上使用公理，但把待证明的结论直接当成未经证明的假设，并不能构成对原问题的解决。因此，“存在公理”不能一概判为错误，“能够通过检查”也不能脱离它依赖的假设来理解。官网规则把公理审计列入核验流程，并把命题失真、占位或未经审核的公理等列为可能撤销奖项的原因。

就奖项而言，官网 v1.0 将 Lean 验证设为评审准入门槛，最终评奖仍由组织委员会决定。规则还区分完整解决与部分进展：改善某个界限、完成某些特殊情形，可以是有价值的工作，但不能因此宣称整个问题已经解决。

奖金也不能只看标题中的数字。Pinnacle 档规定每项符合条件的完成结果对应 100 万美元奖池，其余档位的金额由委员会评审确定。付款另有身份与合规核验要求。因此，机器验证通过、正式获奖与奖金支付，是需要分别确认的状态。

参加孙宇晨奖，必须用 AI 吗？

不必须。官网 v1.0 规则允许人类、人机协作和自主 AI 等不同方式参与。自主 AI 参与也需要由符合要求的自然人、法人或授权代表承担申请与收款等法律责任，不能把“AI 可以参赛”理解成一个模型账号就能直接领奖金。

验证工具则有明确限制：按这版规则，Lean 验证是评审准入要求，Coq、Isabelle/HOL 等其他系统的结果可作补充，不能替代它。这是该奖项的提交规则，不代表其他证明助手在数学上没有价值。对于已经公开发布、获得广泛同行验证与认可的 Lean 成果，规则另设登记和时间戳路径；实际提交前还应核对官网的现行流程。

不参与解题，也能看懂哪些进展？

普通读者不必先学会 Lean，也可以从成果描述中抓住几个具体问题：提交的是新证明，还是已有证明的形式化？覆盖了完整命题，还是某个特殊情形？是否提供了可供复核的命题、代码和检查材料？如果报道声称已经获奖，能否找到对应的正式公告？

下次刷到“AI 攻克数学难题”的消息，先别急着开香槟，看看它到底交出了哪一层成果。把已有证明写进 Lean，本身可以很有价值，却不等于第一次解决了这道题；通过机器检查，也还要核对原题和评奖结果。能找到公开命题、证明代码和正式评审信息，才有材料继续判断。

进一步阅读

奖项官网：https://www.hejustinsun.com/zh/prize

评选规则 v1.0（2026 年 9 月 16 日生效）：https://www.hejustinsun.com/zh/prize/rules

Lean 官方介绍：https://lean-lang.org/

《Theorem Proving in Lean 4》导论：https://lean-lang.org/theorem_proving_in_lean4/Introduction/

公理与计算章节：https://lean-lang.org/theorem_proving_in_lean4/Axioms-and-Computation/