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

孙宇晨奖（The Justin Sun Prize）是孙宇晨个人出资、围绕数学题单设立的奖励计划。规则把解题与 Lean 形式化贡献分开分配奖金，讨论的也是两个不同问题：证明怎样找到，又怎样让别人可靠地检查？先从一道整数题看这两件事的区别。

算对很多例子，仍要回答“为什么总成立”

对任意整数 n，n²+n 都是偶数吗？代入 1、2、3、4，得到 2、6、12、20，看起来没有问题。即使程序继续试算一百万个整数，也没有仅凭这些例子覆盖无限多个整数。

证明可以从下面的等式开始：

n²+n = n(n+1)

1. n 与 n+1 是相邻的两个整数。
2. 相邻整数中必有一个是偶数。
3. 乘积因此能被 2 整除，n²+n 就是偶数。

这条理由适用于任意整数，不必逐个尝试。若命题本来只涉及一个明确的有限集合，可靠地枚举全部情况也可以成为证明的一部分；关键是计算范围能否覆盖命题承诺的范围。

AI 可以寻找反例、提出猜想，也可以尝试推导。某个实例算对、一段文字看起来像证明，以及论证对全部给定情形成立，需要分别判断。用了一个不满足条件的定理，后面的文字再流畅也补不上缺口。

Lean 检查什么，形式化者要补什么

Lean 是编程语言和证明助手。使用者精确写出对象、命题和证明，内核再按系统规则检查证明对象。它把解释性的文字转换为可检查的形式化内容；不能只凭推导“看起来合理”过关。

把整数题交给证明助手，要明确 n 的类型、偶数的定义，再连接因式分解与奇偶推理。实际工作可以调用数学库中的定义、定理和自动化工具，不必手工展开每个最基础的步骤。

从思路到可检查成果

1. 探索：尝试例子、找反例，选择可能用到的定理。
2. 组织证明：把前提、中间结论和最终结论接起来，补齐关键推理。
3. 形式化：把对象、条件与证明写成 Lean 能处理的内容。
4. 检查并对应原题：检查推导，同时确认形式化表达没有改变原问题。

这些工作会来回进行。形式化时发现少了条件，需要回头改证明；探索时找到反例，研究方向也可能随之改变。人和 AI 都可以参与多个环节，提出答案与检查答案则各有任务。

论文里省略的步骤，需要有可检查的依据

读论文时，“类似可得”或“显然成立”可能依赖读者的背景知识。形式化时，需要写出依据，或用可检查的自动化过程补上。做除法要处理分母为零的情况，使用只适用于有限集合的定理要确认对象满足条件；这些要求不表示原证明必然有错，却会影响其能否完整表达。

Mathlib 等已有数学库可以减少重复工作，但找到适用定理、核对条件，再把论文表述与库中的定义对应起来，仍需要数学理解和工程工作。形式化者做的不只是把自然语言换一种拼写。

70% 与 30%，对应两种贡献

按 2026 年 10 月 7 日读取的官网规则，分配方式是：

• 解题者获得 70%：完成题目所要求的数学结果。
• Lean 形式化贡献者获得 30%：完成形式化，并按要求提交通过验证的 PR。
• 同一主体完成两项：获得该题分配奖金的 100%。

PR 是向代码仓库提交修改、请求审核合并的方式。这里的“形式化贡献者”是完成形式化并提交成果的人，不能与主办方审核材料的人员混为一谈。擅长找证明和擅长形式化的人，可以围绕同一道题协作。

30% 的分工，让补条件、找定理和对齐定义有了单独的奖励。如果成果还提供了其他研究可复用的定义与引理，价值可能延伸到原题之外；这属于机制潜力，实际效果仍要看提交和成果积累。

机器通过了，还要分清这三层

推导是否在给定前提下成立？

形式化检查在写明的定义、条件和公理下进行。Lean 可以在明确的逻辑基础上使用公理，不能因此把“有公理”一概当作错误；但若把待证明的结论直接当成未经证明的假设，也没有解决原题。证明的依赖仍需审计。

检查的命题是否就是原题？

假设原题是“对任意整数 n，n²+n 都是偶数”，提交时却额外要求“n 是偶数”，即使证明通过，也只覆盖了部分情况。机器不会替我们判断，这个更窄的命题是否已经回答原问题。

类似地，改善一个界限、处理某些特殊情形，可以构成有价值的部分进展，但不能据此宣称完整难题已经解决。

是否达到评奖与付款条件？

奖项将 Lean 验证作为评审准入门槛，而非最终评奖结论。提交、资格、贡献归属与评审仍按奖项规则处理，最终授权由组织委员会决定。官网也把命题失真、占位或未经审核的公理等列为可能撤销奖项的原因。

Pinnacle 档规定，每项符合条件的完成结果对应 100 万美元奖池；其他档位的分配金额由委员会评审确定。奖池按上述贡献分配，付款另有身份及合规核验要求。因此，验证通过、正式获奖和完成支付，是三个需分别确认的状态。

参与方式可以不同，提交门槛仍要满足

奖项允许人类、人机协作和自主 AI 等不同方式参与，不要求必须使用 AI。自主 AI 的申请、授权代表和收款责任，仍要由符合要求的自然人、法人或书面授权代表承担。

Lean 是这项奖的验证要求。Coq、Isabelle/HOL 等系统的成果可以作补充，不能代替 Lean 准入条件；这是奖项规则，不是对其他证明助手数学价值的否定。

已公开发布、获得广泛同行验证与认可的 Lean 成果，规则另设登记与时间戳路径。其他提交按官方 PR、验证与评审流程处理。本文说明贡献和检查的区别，具体参加时仍需核对现行流程、材料及资格条件。

看“AI 解题”新闻，先看交出了哪一种成果

• 提交的是新证明，还是把已有证明形式化？
• 覆盖完整命题，还是某个特殊情形或更窄的条件？
• 有没有公开命题、证明代码和可复核的检查材料？
• 如果报道说已经获奖，能否找到对应正式公告？

先别急着开香槟。把已有证明写进 Lean 可以很有价值，但不能自动变成“首次攻克难题”；通过检查也还要对应原题。找到公开的命题、代码和正式评审信息，才有材料继续判断。

本文于 2026 年 10 月 7 日对照奖项规则页与 Lean 官方教程整理，奖项条件依据此次读取的规则说明，参加时应核对现行条款。整数例子用于解释证明范围，本文未运行 Lean 验证。

• 奖项官网：https://www.hejustinsun.com/zh/prize
• 评选规则：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/