全面解读孙宇晨奖，及如何参与拿到最高100万美元奖金🔥   我操，孙哥搞了个孙宇晨数学奖，单题奖金最高【100万美元】，船长感觉这会彻底激发民间 AI 解题活力。 个人或小团队的春天来了，AI 行业或迎来结构性利好！！ 我没吹牛哦，给你们盘盘！ -   一、这是在做什么事？   最近不是 OpenAI 攻破了世纪性数学难题，他们采用大规模 agent 攻纳维–斯托克斯并给出 Lean 证书，然后纽约大学一教授指控 OpenAI 模型读取了他尚未公开发表的草稿，是截胡行为。   这就给美国克雷数学研究所制造了难题，他们的千禧年大奖100万美元奖金不知要颁给谁了。虽然 OpenAI 宣称放弃领奖，但依然制造了争议。   孙哥做的事就是把这件事变成了就像是公开标价的施工单，用去中心化、零信任的方式让机器决定谁获奖，这将彻底颠覆传统委员会模式。   这是人类历史上首次把人类数学证明转化为机器可验证形式化证明，而且填补了诺贝尔奖一百余年未设专项数学奖的空白，让数学进入了一个新阶段。 -   二、为什么说个人和小团队的春天来了？   一是因为奖跟着题目走，不跟着人走。不设提名、不论资历与年龄，解决了小团队没资格的痛点。唯一触发条件是机器把证明从第一行核到最后一行，通过即确认获奖资格。   二是因为以往大公司解题是为了证明自己的模型和算力牛逼，最高100万对他们来说可有可无。而对于个人或小团队来讲，最高100万是笔巨款，而且是成名的好机会。   三是这个孙宇晨奖的机制给小团队留了窗口：解题70% +形式化30%。30%那截，就是专门给小团队留的，把已有进展写成能过 Lean 的证明即可。   四是时机有利，时间定义是2026年以来。自动定理证明、autoformalization、Lean agent 已经能把大量中间引理压到人设方向、模型填细节、机器拒错，一个人加几个强模型和一台够用的机器，已经能完成过去所有工作。 -   三、为什么说 AI 行业或迎来结构性利好？   第一，给模型一个硬考场。现在很多 AI 数学成绩停在看起来对，这个奖逼输出必须过 Lean。过不了就没钱，实验室就得把能力从写漂亮证明，改成交可复查证明。这是在推可靠推理，不是推更会聊天。   第二，把最后一公里做成可赚钱的工作。AI 已经能出思路，缺的是有人把思路砌成机器能核的形式。30% 给形式化，等于给这笔累活开工资。有人做，才会有更多过核样本、更好的翻译模型和修复工具。模型下一轮吃的就是这些东西。 第三，把可信从宣传改成交付。以后比的不是谁先发帖，是谁先交出证书。习惯一旦立住，会从数学渗到代码、协议、科研结果，AI 可以很快，但必须能被拒绝、能被复检。 -   四、个人或小团队如何参与？   个人或小团队是最直接的受益者，可以妥妥的吃肉。总共有三种方法：   ➢ 全做：解题 + 写成 Lean，拿全额。难，适合题小、命题清楚。 ➢ 只做形式化：已有公开证明，你负责搬进 Lean，拿 30%。这是小团队主路。 ➢ 只出思路：找到解法，找人写成 Lean，拿 70%。必须事先写清分成，否则过核后会吵。   最简单的就是做第二种，全吃下是很难的，只做形式化，找已有公开证明，你负责搬进 Lean，拿这30%，然后跑量，就把它当工程的分包做，还是很舒服的。   团队配置上，我感觉三人就够，一个数学判断，管命题和证明策略；一个 Lean 工程，管构建和复检；还一个检索与记录，管文献、过程日志、提交材料。两人也行，一个人就白天审题、晚上过核，模型当第三个人用。一个人会比较累，但可以慢慢做。 快的话几周，慢的话几月就能拿到结果。 -   五、入口与工具   【官方入口】 奖项主页：   中文介绍 / 规则：   GitHub 组织：   规则、题单、候选记录：   题库说明：   验证说明：   参与 / 纠错用 Issue：     官网要求：资格前提是向 GitHub 提交并通过核验的 Lean PR。现有 awards 仓库主要是记录，具体证明仓库和 lean-toolchain 以组织下后续仓库为准。   【建议工具】 Lean 4 源码：   安装说明：   手动安装：   版本管理器 elan（装这个才能按仓库切换版本）   构建工具 lake（装 Lean 4 后自带）   编辑器：VS Code + Lean 4 插件 VS Code：   插件：在扩展里搜 Lean 4（发布者 leanprover）