十月三十号到十一月一号，Caltech要办一场活动：一百支团队，分到价值两百万美元以上的前沿模型算力，四十小时内挑战数学界悬而未决的猜想，再向顶尖数学家答辩。官网把它叫做史上第一个面向研究级数学的黑客松。
听起来像一场AI碾压人类数学家的秀。但主办方自己在脚注里写了一个词——unverified。这三个字，才是这场活动真正该被读懂的地方。
一场黑客松，两轮奖
事实很简单：Caltech主办，赞助方提供算力，赛制分两段。
第一段是十一月一号现场答辩，评审是数学家，奖项发给「最有前景、讲解最佳」的团队——这时候评的是表达和思路，不是证明是否成立。第二段要等数学共同体花时间核验之后，再颁一轮奖。换句话说，主办方自己也承认：现场好看的东西，不一定是对的东西。
三项突破，三种熟度
主办方拿来当叙事支点的三项2026年成果，验证程度其实完全不在同一档：
- Erdős平面单位距离猜想.结果是证伪，AI构造出一族点集打破了原猜想的上界，且已经由人工独立核验、重写成论文。这是实锤。
- 首个显式非sofic群构造.以Lean 4形式化证明公开在代码仓库里，能编译、可审计，但常规的同行评审还没走完。证书有了，共识没到。
- 六维球面（S6）存在复结构.目前只是候选声明。它自己的Lean形式化项目里，把论文的关键结果当公理直接引入，边界处还留着两处未完成的「sorry」——这是Lean里明摆着写给自己看的「此处证明未完成」。第三方能重现符号计算，但存在性、光滑性、和S6的全局等同性都没被独立重构。
三件事分属不同数学分支，共同点只是都用AI辅助发现和形式化，并不是同一套理论突破在三个战场同时开花。
Lean编译过，不等于数学界认可
2024年DeepMind的AlphaProof和AlphaGeometry 2在IMO赛题上拿到银牌水平，让外界第一次相信AI能碰结构化数学题；后来Epoch AI推出的FrontierMath，是想把难度拉到更接近真实科研。Lean这类证明助手扮演的角色是「可验证层」——AI写的证明能被机器一步步核对，不用只靠自然语言描述取信。
这套技术演进背后有个容易被忽略的框架：AI把一个命题形式化并通过编译，和AI像数学家一样理解并解决一个问题，是两件不同的事。前者是语法正确，后者是意义成立。S6的两处「sorry」正好卡在这条线上——编译通过不代表全局证明闭环。
编译通过是语法过关，同行评审才是意义过关。
历史上类似的坑不新鲜。1993年安德鲁·怀尔斯宣布证明费马大定理，轰动一时；审稿人很快发现一处漏洞，怀尔斯又花了一年多才补上。公开宣布和最终成立之间，从来隔着一段说不准多长的时间。S6声明现在停在哪一步，谁也不能打包票。
这场黑客松真正测的是什么
主办方把问题设成「AI能不能比数学家更快解猜想」，可现有证据更支持另一个答案：AI在证明搜索、证明检验这两层进步明显，但猜想生成、理论构建这些更高层的能力，还没看到独立自主的证据。三项引用案例里，唯一算「实锤」的那一项，靠的也是人工独立核验，不是AI自证。
- 风险.黑客松第一轮就给「最有前景、讲解最佳」发奖，等于把叙事和讲解能力放在验证之前奖励，容易滑向排行榜优化——谁的PPT讲得好、谁复用了现成的形式化库跑得快，未必等于谁真的做出了数学贡献。人机贡献比例、算力用量，官网目前都没说要披露。
第二轮验证奖是个诚实的设计，承认了「现场好看」和「事后成立」不是一回事。但它解决不了短期炒作：媒体标题、社交传播、赞助方公关，第一轮就已经吃完了红利，第二轮验证结果出来时，声量早就散了。真正该盯的，是S6那两处「sorry」什么时候被填上，非sofic群的证书能不能真的走进期刊，以及赛事最后有没有公开各团队到底用了多少人、多少算力。
那个被主办方轻轻放进脚注的「unverified」，比正文里所有形容词都更值得记住。