2026年7月25日，一个自称“形式化反证”的Lean文件出现在网上，声称著名的考拉兹猜想（Collatz conjecture）是错的。它通过了工具链的层层机械校验，包括专门为抓“作弊证明”而生的Comparator。消息传开，数学界一片哗然。
然而三天不到，真相揭晓。所谓反证，是一个利用Lean内核漏洞构造的伪证。漏洞随后被修复，“证明”失效。考拉兹猜想依然是那个没有被证明、也没有被推翻的猜想。这场闹剧从出现到穿帮，只持续了大约两天半。
半个月后，同一个生态里诞生的另一件事，把闹剧背后的真问题摆上了台面。8月18日，陶哲轩在博客上宣布，由Lean聚焦研究组织（Lean FRO）与ICARM联合孵化的Palomar注册表正式开放投稿。它要做的事情只有一件，给Lean验证过的数学证明建立一份公开、可检索、可审计的登记档案。陶哲轩本人担任科学顾问委员会成员，并已把自己的森多夫猜想（Sendov's conjecture）形式化证明，注册为Palomar的第一个条目。
伪造与立规，同月发生。一退一进之间，AI数学时代最尖锐的问题浮现出来，当证明开始批量生产，谁来负责确认“这是真的”？
证明越来越便宜，信任越来越贵
先看生产端。2026年以来，机器辅助证明与机器辅助形式化的数量与复杂度大幅上升，这是Palomar官方声明开篇就承认的事实。AI解决老问题、新问题的新闻几乎以周为单位出现。此前悬而未决的Erdős问题728、347、369，2026年在AI辅助下被解决，并在Lean中完成形式化验证。据报道，有AI模型生成了推翻雅可比猜想的反例，那是一个悬而未决87年的问题。连Lean自身也成了AI定向找漏洞的目标，并且真的被找到了若干漏洞。微软研究院报告，Lean经由Aeneas工具链，对生产环境的密码学算法SymCrypt完成了形式化验证。
再看信任端。一个Lean仓库要证明“它真的证明了某定理”，对不熟悉Lean的读者来说，需要跨越三重障碍。仓库里声称的形式化命题，是否有真正通过类型检查的证明；证明里有没有塞入额外公理这类作弊；形式化命题与非形式化描述，在语义上是否真的对应。考拉兹伪证在头两层全部“通过”，最终倒在最底层，漏洞不在证明逻辑里，而在Lean内核本身。
这还不是最可怕的。真正的风险在于，当每天都有“AI解决了XX”的声明，普通数学家既没有时间、也没有工具逐一核实。陶哲轩在8月12日的博文里记录过这个过程，AI生成的证明不是为人类阅读准备的，他花了数天时间、借助AI辅助，才把森多夫猜想的证明“消化”成可发表的手稿。据该博文评论区披露，这份证明的Lean代码约9.3万行，其中只有约1.7万行是人工撰写，其余是生成证书的机制代码。一个人要逐行读完9.3万行代码再判断其对错，这已经不是成本问题，而是能力问题。
Palomar解什么，不解什么
Palomar的第一层定位，是“Lean证明的预印本服务器”。这是陶哲轩自己给出的零阶近似。一个外部GitHub仓库以特定commit的“快照”为单位提交，注册后获得永久的条目记录，任何人都能检索、核对、引用。但它刻意不做同行评审，陶哲轩在博文里把话说得很直白。
“需要强调，检查（a）和（b）远达不到真正的人类同行评审对新颖性、趣味性和准确性所做的审查。特别是，Palomar不是一份同行评审期刊。”
机制上，它把“验证”拆成两段。每个仓库必须包含三样东西，用Lean写成的、人类可读的挑战声明文件；任意长度的解决方案模块；以及formalization.yaml，用非形式化语言描述结果，并记录协作者、AI使用情况（包括模型与预算）、许可与署名等元数据。提交之后，第一段检查由Lean FRO开发的Comparator执行，纯粹机械，确认解决方案模块恰好证明了挑战文件声明的命题，即便面对刻意构造的对抗性证明也能安全校验。第二段检查交给大语言模型，比对formalization.yaml的非形式化描述与挑战声明的语义是否匹配。陶哲轩坦承，这一段是“非确定性的”。
这里藏着一个微妙的自我指涉，用AI的增长来治理AI的产出，用非确定性来对冲非确定性。Palomar的回应是，把该透明的环节全部透明。声明与证明分离，读者知道要审计什么。元数据强制披露，作者用了什么模型、花了多少预算，一目了然。Verso文档系统把形式化命题渲染到网页上，鼠标悬停即可查看每个Lean术语的含义。它期望的是最低准入门槛，而不是最终判决。
为什么是现在，为什么是这群人
Palomar诞生的时间点，恰好踩在一条加速曲线上。2021年，一个团队用Lean验证了Peter Scholze凝聚态数学中的关键证明。2023年，陶哲轩与合著者用Lean形式化了自己的多项式Freiman-Ruzsa猜想证明。2026年，AI解决并验证的问题名单还在拉长，AI还被用于支撑费马大定理的Lean形式化工作。从人类把证明写进机器，到机器自己写证明、人类负责把关，节奏以年为单位在换挡。
速度本身不构成危机，信任缺位才构成危机。Palomar官方声明里有一段话，值得每一位关心数学的人反复读。
“每天都有关于机器辅助解决著名问题的大胆声明，却缺乏充分的审校、充分的透明度和充分的语境。这种情况正在制造混乱，同时侵蚀着我们对‘已确立的数学事实’的现行标准。”
混乱的治理方式无非两种，要么由共同体自己设定标准，要么让标准在野外自发形成，或者由价值观与数学进步相冲突的外部力量强加。Palomar声明给出了明确立场。
“数学共同体必须保留其设定标准的中心角色，而不是让标准在野外自发形成，或由价值观与数学进步相冲突的外部力量强加。”
科学顾问委员会九人名单本身就是信号。Jeremy Avigad、Akshay Venkatesh、Ravi Vakil、Bryna Kra、Kim Morrison，加上陶哲轩，集合了逻辑、数论、代数几何、动力系统多个方向的一线数学家。这九个人不是在给某个公司的产品站台，而是在给“数学共同体自己定标准”这件事背书。Lean生态的机构动能也在同步积累，2026年7月，亚马逊自动推理部门宣布向Lean FRO捐出该组织历史上最大的一笔捐赠；对生产级密码学代码的验证，则把形式化从纸面拉进了真实的软件供应链。
没有裁判的安检门
Palomar的边界和它的价值一样清晰。Comparator是机械的，但机械不意味着绝对。考拉兹事件的教训说明，内核本身可以有漏洞，而且这种漏洞可以长时间蛰伏在稳定版本里。LLM语义检查是非确定性的，它可能放过语焉不详的声明，也可能误判完全正确的对应。它连自己都审，Palomar的第一个条目，自动评审给出的反馈就指出，关于证明新颖性的声明缺乏文献检索支撑，建议将其限定为未知。注册表不为任何条目做新颖性和相关性背书，官网把它写得明明白白。
它也不是孤军奋战。ProofAtlas上还存在一个与陶哲轩版本零代码共享的森多夫猜想独立形式化，1160个文件、92816行代码、单条主定理，由Lech Mazur完成并经Lean验证。两个独立团队、两套完全不同的代码、验证同一个定理，这种“双重证据”正是形式化生态最健康的形态。Palomar要做的，就是让这类证据可检索、可引用、可信任。它把“验证”从个人手艺变成公共基础设施，期刊可以把它当作overlay层使用，审稿人把稀缺的精力留给概念新颖性与证明优雅，基础逻辑的机械正确性交给机器。这是分工，不是替代。
底线由谁定，数学就由谁定义
回到那个2.5天的闹剧。考拉兹伪证最值得玩味的地方，不是它骗过了工具，而是它差点骗过了整个社区对“机器验证”的信任。如果“验证”本身不能自我治理，那么当AI批量产出证明的浪潮彻底到来时，被稀释的将不只是个别结论，而是数学这门学科的信用基础。
Palomar给出了一个务实的回答，把底线写成代码。最低标准可以是工具检查加人工复核，可以是强制披露的元数据，可以是像arXiv一样粗粝但持久的公共记录。门槛设得越低，越多人能进入这个生态，提交自己的形式化证明，无论它来自人类、来自AI、还是两者的混合体。陶哲轩在博文里对三类提交都表示欢迎。
AI对数学的冲击，不会停留在“AI能解多少难题”。更深层的改变是，机器正在把“证明”变成一种可以规模化生产、检验、交易的东西，数学界必须回答，在这样的世界里，什么仍然不可替代。答案从Palomar的设计里已经浮现，证明可以交给机器，标准必须留给人。数学界正在把“信任”工程化。
这道工序省不得，也骗不了人。
快报