如果从传统数学史看，数学的发展可以讲成代数、几何、分析、概率、拓扑、逻辑不断分化又统一。但如果从计算机和 AI4Math 看，近十年的主线更像一部数据集形态变化史。
一开始，AI 做数学主要是在回答题：给出最终答案，算 exact match。后来，数据集开始要求模型写过程、生成多条解法、接受 verifier 打分、调用代码执行器、进入 Lean/Coq/Isabelle 这样的 proof assistant，最后又发展出 live leaderboard、去污染评测、研究级问题和提交制 formalization 平台。
换句话说，前沿不只是“模型更会做题了”，而是数学数据集本身从静态题库变成了可执行、可验证、可审计、可持续更新的数学工作流。
上一篇我们做的是新闻核验：OpenAI 最近公开的 Astra 十项数学结果，究竟是不是“新模型解决了十道著名数学题”。结论是：事情基本属实，但流行说法太粗糙。
这篇换一个问题：如果不看标题党，这十个问题本身到底在研究什么？
它们横跨高维几何、编码理论、群论、算子代数、代数复杂性、量子信息、格算法、凸几何和极值组合。读者很容易只记住“十个难题”，却不知道每一项究竟难在哪里、研究史卡在什么地方、Astra 到底推进了哪一层。
所以这篇是总览：把此前十份专题调研压成一篇大博客，每一项都给一个相对完整的概要。
2025 年 10 月，OpenAI 曾闹过一次很难看的数学误报：公司高管把 GPT-5 找到十道 Erdős 问题的既有文献解答，说成了“解决十道此前未解的问题”。数学家 Thomas Bloom 当时称这是 “a dramatic misrepresentation”，相关帖子随后被删除。
不到一年后，OpenAI 又带着“十道开放问题”回来了。
这一次，材料完全不同：一份 249 页技术文稿、一份 62 页思路说明、十个大型 Lean 文件、十二组 Comparator challenge，以及 OpenAI 对正确性的公开责任声明。产生论证的模型叫 Astra，是 OpenAI 尚未发布的下一代内部模型。
如果这些结果经受住外部审查，这会是 AI 数学从“偶尔参与一篇论文”跨向“同一个通用系统批量产生研究级新数学”的重要节点。
但新闻标题“新模型解决十道著名数学题”仍然漏掉了几乎所有关键限定。
到 2026 年 7 月底，再问“今年还有哪些会能投”，最容易得到两种错误答案。
一种只按全文截止日期排序，于是把 mandatory abstract 已经过期的会议也算成“仍开放”；另一种只搜索 CFP 里有没有 AI for Math，于是错过 WSDM、FSE、CAV、IUI 这类名字不直接写数学、却可能非常适合的会议。
更麻烦的是，这里说的“2026 下半年可投”，大多是投稿截止发生在 2026 年、会议在 2027 年举行，而不是只找会期在 2026 年的会议。
2026 年 6 月，Tau Ceti 还是一个新仓库。到 7 月 31 日的固定快照，它已经有 932 个 Lean 源文件、171,565 行代码和 1,336 个已合并 PR。在最忙的一天，100 个 PR 进入 main。
如果只看这些数字，Tau Ceti 很容易被概括成“AI 正在复制 Mathlib”。但我把它的五个组织仓库、Worker、review archive 和依赖更新链条全部拉到本地后，发现真正值得研究的并不是 AI 写 Lean 有多快，而是它怎样重组了一座数学库的生产关系：
人类写 roadmap 和 rubric，AI 写代码、修代码、审代码；Lean kernel 与 trusted CI 负责机械裁决；每一次 review 都成为公开数据。
这不是一个更大的 theorem-proving benchmark，而是一套正在运行的 formal-library operating system。
2026 年 7 月，ICM 在费城开会时，AI 已经不再只是数学大会外围的技术展示。Terence Tao 谈“AI 时代的数学”，Alex Kontorovich 谈数学的未来形态，会场还把 Mathematics for AI 和 AI for Mathematics 拆成两场方向相反的圆桌。
几乎在同一时间，另一批更具体的变化正在发生：开放猜想被整理成 Lean 语句，真实数学仓库中的 sorry 被做成动态 benchmark，最新 arXiv 论文里的 lemma 被实时抽取，模型也开始参与形成研究预印本。
但“AI 已经开始解决开放猜想”这句话仍然需要拆开。它可能指奥赛题，可能指把已知证明翻译成 Lean，可能指找到一个更好的有限构造，也可能真的指一个此前未知的数学结论。这四件事的证据强度完全不同。