孙宇晨奖是什么？读懂 AI 数学悬赏、Lean 验证与获奖规则

孙宇晨奖（The Justin Sun Prize）是由孙宇晨出资、围绕数学题单设立的悬赏计划，既奖励解决问题的人，也为把证明转成机器可检查形式的贡献分配奖金。它最值得关注的地方，是让形式化工作获得独立报酬。不过，“机器验证通过”和“最终拿到奖金”之间仍有评审与付款条件。读懂这几层关系，才能理解这项计划的价值与边界。本文依据 2026 年 9 月 16 日长文、官网 v1.0 规则及公开记录整理。

两种贡献，两栏署名

在《我为什么要设立孙宇晨奖》中，孙宇晨把设奖描述为将来自数学的财富回馈数学。他提出以题目为中心的奖励方式：一栏记录证明者，另一栏记录形式化者，允许人类、AI 及人机协作参与。同一主体可以承担两种角色。

这种分工有具体含义。发现一个证明，需要找到解决问题的思路；完成形式化，则要把命题、定义和推导写到证明助手能够处理的程度。纸面上被省略的条件或中间步骤，到了形式化环境里往往需要补全。这可不是把论文换个格式上传：缺了定义、漏了条件，都得有人补上。形式化本身就是一份需要数学理解与工程工作的贡献。

官网规则第 5 节给出的分配比例是：解题者获得该题分配奖金的 70%，Lean 形式化验证者获得 30%；同一主体完成两项，则获得全部分配奖金。这里的“验证者”指完成形式化并提交通过验证的 PR（Pull Request，即向仓库提交修改并请求合并）的贡献者，不应与组织方负责审核的人混为一谈。

孙哥愿意为数学出钱，当然值得关注；但看奖金，还是得把档位和条件一起看。Pinnacle 档规定每项符合条件的完成结果对应 100 万美元奖池；其余四档的金额由委员会评审确定。不能把“Pinnacle 档百万美元”改写成“所有题目都悬赏百万美元”，也不能把题单中的每个条目都视为已经确定金额的可领取任务。

Lean 检查了什么

Lean 是一种开源编程语言和证明助手。与让聊天模型评价“这段证明看起来是否正确”相比，形式化验证要求把陈述与证明写成精确的形式，由检查内核验证推导是否成立。AI 可以帮助探索思路或生成形式化内容，但输出仍须接受检查。说得直白一点，不能让 AI 写完证明，再由它自己拍胸脯说“没毛病”。

这把两个问题分开了：给定命题的推导是否成立，以及写下来的命题是否准确表达了原问题。第一项可以交给形式化检查承担重要工作，第二项仍需要对照原始文献、定义和条件。若最初就把问题写弱了，证明一个较弱命题并不等于完成原挑战。

官方仓库的 Issues（用于提交问题与讨论的议题区）中有一个容易理解的例子。Issue #57 的提交者指出，JSP-000199 的题目描述缺少一般位置约束，并提出应补充“无三点共线、无四点共圆”等条件。该 Issue 引用的题目问的是：能否找到一个平面点集，让不同距离的出现次数恰好分别为 1 到点数减 1。

给题目“挑刺”，有时比急着解题更重要。为什么一个条件会改变问题？按 Issue 引用的简化表述，把四个点等距放在直线上，距离 1 出现三次，距离 2 出现两次，距离 3 出现一次，就已经得到 1、2、3 这组出现次数。这个小例子说明省略几何限制可能让问题变得过于容易，却不证明原数学难题已经解决。

截至本次阅读，该 Issue 仍为 Open；这是社区提交的纠错意见，不能写成主办方已经认可的结论。官网规则也把命题失真、占位或未经审核的公理、错误定义造成的空洞结论等列为可能撤销奖项的情形。这恰好说明，可信验证需要检查推导，也需要守住“究竟在证明什么”。

长文与规则对照

X 长文强调机器核验、题价锁定和尽量减少人为干预；官网同日生效的 v1.0 评选规则则列出委员会、评奖和付款流程。把两者并列阅读，比只引用其中一边更接近参与者实际面对的信息。

这些表述之间的适用关系需要主办方进一步说明：是否属于不同层级的规则，是否存在需要同步的版本，或者哪些承诺将由另行公布的机制落实。现有材料没有明确解释这些条款如何衔接。参与者尤其需要确认：历史成果的解题与形式化两种贡献分别适用什么时间边界，而不能仅凭长文或一条追溯条款推定自己有奖金资格。

对准备投入时间的研究者而言，实际重要的是先确认对应题目的资格、奖励范围与提交要求。官网规定仅认可 Lean 形式化作为准入依据，Coq、Isabelle、HOL 等其他证明助手中的成果只能作为辅助背景；已公开且获社区认可的 Lean 形式化另有登记与时间戳核验路径。因此，“开放参与”不等于任何形式的成果都自动满足条件。

委员会也并未从流程中消失。规则第 2.3 节描述 AI 模型与领域专家参与，其中 AI 提供初步评估和建议，最终评奖由组织委员会决定。第 4 节列出三个评价维度：问题悬而未决的时间、成果发表渠道的严谨性与地位、数学界的认可程度；具体阈值和详细程序仍不公开。第 5 节同时说明，发表渠道、形式及是否已发表不作为获奖前提，因此“评价时参考发表渠道”不能改写成“必须先在指定期刊发表才能申请”。就当前文件而言，把它概括为完全无人工裁量的自动派奖系统并不准确。

规则第 4.2 节还区分完整解决、实质解决、部分进展和无进展。完整解决可以是证明、反驳或其他结论性解决；改进参数界限或处理特殊情形属于部分进展，不能宣称整道题已解决。奖金会结合完成状态调整，无进展不具备获奖资格。因此，仅有机器通过的结果，还不足以让外部读者自行计算应得金额。

怎样读 GitHub 记录

官方 awards 仓库是问题、证据、候选和已公告奖项的公开记录入口。它的价值在于让信息可以被引用、纠错和追踪，而仓库页面上的一次活动不必然代表研究突破。

参与说明列出推荐题目、推荐获奖者、纠错和争议四类 Issue，并明确提醒：提交 Issue 或通过仓库检查，不构成获奖公告；仓库检查成功也不认证数学内容。

读到“有人提交了证明”时，可以按下面的顺序判断它到底到了哪一步：

1. 先看记录类别。例如 JSP-000199 对应的 #57 是 Correction，讨论的是题目表述；它不是一条已宣布的获奖记录。
2. 再看证据对象。区分原始问题、论文、形式化代码和验证记录，注意代码是否指向固定版本，以及证明覆盖的是完整问题还是特殊情况。
3. 然后看处理结果。Open 表示议题仍开放；Closed 或 PR 合并也不能单独证明已经获奖，要阅读维护者回应和状态变更理由。
4. 最后找正式公告。仓库将 candidates 与 awards 分开保存。只有对应公开公告的正式奖项记录，才支持“已经宣布获奖”的表述；付款是否完成还需要另看付款证据。

这条路径也适合普通读者：不必先具备审查高等数学证明的能力，就能避免把推荐、纠错、候选、正式奖项和支付混成同一个状态。若要实际提交，须继续按当期公告准备材料；公共 Issue 不应包含身份证件、私人联系方式或付款资料。

从核验到付款

按照官网第 6 节，通常的提交路径包括：提交带 Lean 命题、证明与证据包的 PR，由指定验证者在隔离环境核查，再通过 PR 确定资格和优先时间戳，进入评审。其中还提到公理审计与独立检查。所以，跑通不等于到账：核验过关之后，还得看评审结果和付款条件。

正式公告之后也仍有复核环节。官网第 7 节允许获奖者或第三方在公开披露后的 30 天内，就档位、贡献归属、形式化验证结论或获奖者认定等事项提出异议，由未参与原评审的委员复核。奖项可以在公开理由与证据后撤销；规则称已发奖金原则上不追回，撤销记录会与原奖项并列保留。这与“支付记录不可更改”是两件事：交易历史留下来，不代表奖项评价永远不会修正。

奖金支付方面，规则列出 TRC-20 USDT 或 ERC-20 USDC 两种方式，每次付款只能选择其中一种；获奖者还须满足身份及合规验证要求。即便解题主体是自主 AI，申报代表与收款人仍需由自然人、法人或书面授权代表承担。文章中的“AI 可以参与”因此不意味着模型可以绕过身份与收款安排独立领取奖金。

X 长文称首期奖池已经上链，并强调地址和付款记录可公开查询。本文没有独立核对对应资金地址、余额、控制权限或实际支付交易，因此不把“资金已经不可撤回”“验证后自动支付”作为已确认事实。公开余额能回答钱是否在某个地址上，却不能单独回答谁有权转走、按什么条件支付，以及争议发生时怎样处理。

它值得关注在哪里

这项计划有价值的尝试，是把形式化劳动作为可以独立署名、分配奖金的贡献。若执行稳定，它可能为已有数学证明补齐机器可检查的版本，也可能让擅长寻找证明与擅长形式化的人更容易协作。这是机制带来的可能收益，仍需后续成果来验证。

真正能积累可信度的，是命题描述准确、证据可以复核、贡献归属清楚，以及按已说明条件执行的奖励记录。题单规模、Issue 数量或社交传播可以体现关注度，不能替代这些结果。对规则差异的公开解释，同样是参与者判断是否投入时间的重要依据。

对关注 AI 的读者，孙宇晨奖提供了一个具体观察窗口：AI 生成的答案怎样变成可检查的成果，可检查的成果又怎样进入现实中的奖励制度。技术验证提高了结果可复核的程度，但评奖和付款仍有各自的制度条件。把这两部分都讲清楚，才谈得上理解“证明即付款”的承诺要如何落地。

原始资料

• 孙宇晨长文《我为什么要设立孙宇晨奖》：https://x.com/justinsuntron/status/2100134007984029904
• 奖项官网：https://www.hejustinsun.com/zh/prize
• 评选规则 v1.0：https://www.hejustinsun.com/zh/prize/rules
• Lean 官方介绍：https://lean-lang.org/