这是什么地方？
2026 年 10 月，一个未公开的内部数学模型产出了这座「矿藏」：719 篇数学手稿、372 个成果家族，其中约 42%（300 个顶级结果）已经翻译成 Lean 语言、可以被机器一行行验证。剩下的部分「可能有错」——原仓库自己也是这么说的。
怎么逛这张图？
- 想看热闹 → 去「镇馆精选」，十个最重口味的成果，每个都有一段说人话的解读。
- 想查领域 → 「学科地图」按数论、几何、概率……分好类了。
- 想较真 → 「可信度指南」教你分辨哪些结论是机器盖过章的，哪些只是「模型说得很有道理」。
- 想吃瓜 → 「撤稿史」：2026-10-07 刚撤了 3 篇（一个正负号错误连坐的），修了 14 篇。
👑 镇馆十大精选
从 372 个家族里挑出的最重量级战利品。每条都附人话导读。
🧭 学科地图
372 个成果家族按内容关键词自动归类。数字是家族数。
📚 全部成果（372 个家族）
🛡️ 可信度指南（这站最值得看的一页）
数学论文「说它证完了」和「真证完了」是两回事。这座仓库的聪明之处，是给每个结论配了一套机器安检系统。
三档可信度，一眼分清
🟢 第一档：机器验证（本站绿色标签）
结论被翻译成 Lean 语言，由一个叫 Comparator（比对器）的程序自动检查。机器只认逻辑，不认作者脸色——通过了就是真通过。全库 42% 的顶级结果是这一档。
🟡 第二档：有手稿、无形式化（黄色标签）
有完整的论文 PDF，但还没有机器安检。原仓库明说这些「could have issues」（可能有错）。可以看，别全信。
🔴 第三档：已撤稿
被发现问题后公开撤回，但论文还挂在原地、带着「已撤」告示和问题说明。不删帖、留案底。
安检系统里最狠的一招：公理白名单
每个机器验证配置里有一张「许可证清单」（permitted axioms）：证明只许使用三个标准公理（propext / Quot.sound / Classical.choice）。想偷加一条公理把结论「规定成立」？比对器直接判不合格。翻译成人话：不许在考试前偷偷改考纲。
边界声明纪律
每篇 Lean 文档都明确写了「证明了什么」和「故意没证明什么」。比如证明了 π 的无理指数 = 2，但特意注明：Flint–Hills 级数收敛这类推论不随之成立。不许「顺手暗示」。
给普通读者的三句话
- 看到绿色标签 → 可以放心引用「已被机器验证」。
- 看到黄色标签 → 说「有论文声称，未经机器验证」。
- 任何时候都别只因为「AI 写得很自信」就当真——这座仓库自己都撤过 3 篇。
📝 撤稿与修复史
2026 年 10 月 7 日，仓库做了一次大扫除。这是数学界罕见的「公开处刑」，也是这个库最值得尊敬的地方。
撤稿 3 篇：一个正负号的代价
《分裂阿贝尔八重积上 Weil 类的代数性》里一个符号错误，击穿了一个稳定化迹消没论证，连坐两篇依赖它的论文（K3 曲面的 Kuga–Satake 对应代数性、K3 曲面乘积的有理霍奇猜想）。三篇全部公开撤回，原文保留并挂说明。
修复 14 篇 + 联动更新 13 篇
修复范围包括：Lipschitz 高度与 Ashkin–Teller 流的 4 篇（交叉/边界吸附/条件化/收敛论证）、Kähler 极小模型纲领的 6 篇（正定性论证扩充）、驯服与超辛形变的 2 篇（锥等式断言纠正）等。13 篇引用这些成果的论文联动更新了版本。
同日新增 6 个形式化
机器验证覆盖率提升到 300/719 ≈ 42%。撤稿、修复、加固同一天发生——错误不是被藏起来，而是被当众处理。