# 孙宇晨数学奖设1022题悬赏形式化证明

- 来源：AYi (@AYi_AInotes)
- 发布时间：2026-09-16 18:21
- AIHOT 分数：49
- AIHOT 链接：https://aihot.news/items/cmu3yy8230ktsroc1if99g2gc
- 原文链接：https://x.com/AYi_AInotes/status/2100168082249433218

## AI 摘要

孙宇晨新设数学奖挂出1022道题库，采用GitHub PR流程，将奖金直接绑定题目而非个人，每道题分设证明者与形式化者两栏公开署名，人、AI或人机协作均可提交，需机器全程核验通过才触发资金。

## 正文

大家别把孙哥新设立的数学奖当成普通公关，翻开它挂出的 1022 道题库和 GitHub PR 流程，你会发现这套机制真正要做的事，是给 AI 时代的数学形式化苦力明码标价。

做形式化验证、关注 AI 符号推理的人，值得先抽干水份看一遍这套学术结算协议的底层骨架。

它表面是在学诺贝尔奖悬赏未解难题，实际把传统的学术承认链条切成了两截：

1️⃣ 结算对象从人挪到了题目 传统数学奖四年敲一次钟，评选看资历、圈子和同行承认；这套规则把钱死死焊在题目上，每道题设置两栏公开署名：证明者与形式化者。人可以写，AI 可以写，人机协作也能提交。题目一旦上架标价锁定，只有机器从第一行核验到最后一行，资金才会被触发。
2️⃣ 真正的买盘不是天才灵感，而是代码搬砖 这是全篇最聪明但也最现实的一步：已经被佩雷尔曼攻克、甚至拒领过奖金的庞加莱猜想，在这个榜上依然标着 100 万美元。按规则，历史已解决的题目不发发现奖，钱全部留给形式化者。它改变的不是谁来挑战黎曼猜想，而是给数学界目前最脏、最慢、最缺乏明星效应的工种——把几百页的人类纸面证明一行行搬进 Lean 系统的体力活，直接开出了天价悬赏。

3️⃣ 零信任是修辞，执行层依然留着安全阀 比较克制的一点是，大家别真以为能靠自动脚本刷钱。官方 GitHub 仓库白字写得清清楚楚：一次成功的代码编译，不等于数学逻辑正确，不等于有权拿钱。除了顶级题目外，其余金额与完成度仍由委员会终裁，领奖环节还卡着完整的实名合规。此外，千题库里甚至出现了把三维 Navier–Stokes 错标为已解决的瑕疵，仓促上架的痕迹很重。
过去大家以为 AI 数学最缺的是算力跑模型，后来才发现瓶颈在于缺乏机器能验证的高质量基准语料。

模型继续迭代，证明的思路可以成千上万，但能把人类已有的真理沉淀为机器可继承代码的工人，才是目前最稀缺的生态位。
评判一个学术奖项能不能立住，不取决于出资人的名字有多大争议，而取决于那张空着的形式化清单上，未来能不能被严肃学者交出的代码填满。

### 引用推文

> H.E. Justin Sun 👨🚀 🌞：https://x.com/i/article/2099804047448686592