到 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。
理想中的知乎发布流程应该很简单：文章放在 Git 里，服务器执行一条命令，系统找到对应的知乎文章，更新正文和图片，留下日志，最后等人确认发布。
但真正把它做成长期服务，会遇到四个比“Markdown 怎么转 HTML”更难的问题：知乎是否提供稳定的写入契约、登录态应该放在哪里、怎样保证每次更新的是同一篇文章，以及失败以后如何判断远端到底有没有成功。
2026 年 7 月 30 日，Timothy Chow 在 MathOverflow 发了一个标题很直接的问题：Are we stuck with Lean?
截至本文抓取页面时，这个刚出现一天的问题已有 39 票、超过 1.6 万次浏览、6 个回答。它紧跟在 Lean 的 Collatz-themed soundness 事件之后：一份 AI 参与生成的 artifact 同时穿过了当时的 Lean kernel 与旧版 nanoda。于是一个工程事故很快被推到更大的问题上：
Are there any prospects for any organization to seriously support an alternative to Lean?
如果只按标题回答，讨论很容易变成两种口号：Lean 已经赢了，接受现实；或者 Lean 有过 soundness bug，应该换成 Metamath。六个回答和几十条评论真正说明的是：“被 Lean 锁定”不是一个 yes/no 问题，因为这里至少有六种不同的锁。
短期内，数学形式化确实在 Mathlib、工具链和共同体层面形成了很高的 switching cost；但这不等于 Lean 的 kernel、逻辑基础或今天的实现会永远不可替代。比“全部迁移”更现实的目标，是降低不可逆性：让重要证明能被独立 checker 复核、能跨系统重建，让替代生态得到长期工程投入。
MathOverflow 讨论仍在变化。本文中的票数、浏览量和回答数是 2026 年 7 月 31 日的快照；观点均按作者归属，不代表 MathOverflow、Lean 社区或本文的共同结论。
AutoResearch 最容易被描述成一条越来越长的流水线：搜论文、提 idea、改代码、跑实验、画图、写 LaTeX，再让另一个模型 review。按照这个口径，覆盖阶段越多，系统就越接近“AI Scientist”。
但两个代表项目给出了相反信号。
karpathy/autoresearch 只允许 Agent 修改一个 train.py，每轮训练 5 分钟，只看一个 val_bpb；AI Scientist-v2 则从主题、idea 和文献一路走到实验树、论文与 review。后者的行动空间大得多，官方 README 却明确提醒：开放探索的成功率低于模板更强的 v1，有强起始模板时也不一定生成更好的论文。
这不是“简单 Agent 比复杂 Agent 聪明”，而是两套系统承担了不同的验证债务：Agent 每多获得一种行动能力，系统就必须多证明一件事——它没有因为扩大搜索、重复看分数、选择性报告或自我审查而制造假改进。
2026 年 7 月，ICM 在费城开会时，AI 已经不再只是数学大会外围的技术展示。Terence Tao 谈“AI 时代的数学”，Alex Kontorovich 谈数学的未来形态，会场还把 Mathematics for AI 和 AI for Mathematics 拆成两场方向相反的圆桌。
几乎在同一时间，另一批更具体的变化正在发生：开放猜想被整理成 Lean 语句，真实数学仓库中的 sorry 被做成动态 benchmark，最新 arXiv 论文里的 lemma 被实时抽取，模型也开始参与形成研究预印本。
但“AI 已经开始解决开放猜想”这句话仍然需要拆开。它可能指奥赛题，可能指把已知证明翻译成 Lean，可能指找到一个更好的有限构造，也可能真的指一个此前未知的数学结论。这四件事的证据强度完全不同。
2026 年 7 月 28 日，Lean Zulip 的 lean4 stream 出现了一个很难忽略的 topic：Counterexample to the Lean Conjecture (Soundness Bug)。
帖子里的三个事实放在一起，几乎像一道故意设计的判断题：
sorry，#print axioms 没暴露隐藏公理，当时的 comparator.live 和旧版 nanoda 都接受了它。False。这不是“形式化验证忽然失效”的故事，也不是一个模型真的完成了世纪数学突破。它更具体，也更值得研究：一份 proof artifact 把 Lean 官方 kernel 的漏检 与 旧版 nanoda 的另一处漏检 拼在一起，恰好穿过了两套原本彼此独立的检查。
一份不可信的 Lean 项目能够 lake build，不等于它证明了你以为的 theorem。
它可能重新定义了 statement 里的 identifier，用 macro 或 notation 改变表面语法的含义，用不同 typeclass instance 让同一个类型别名展开成另一项，也可能在 build 阶段运行 meta code、写文件，最后再把 sorry warning 藏起来。Lean 很灵活，这种灵活性对正常开发是能力，对 adversarial proof 则是攻击面。
Comparator 的工作，是在一个 reviewer 控制的 theorem statement 与 untrusted proof project 之间建立边界。它不只问“这份代码能否编译”，而是问：它是否证明了 trusted Challenge 中那个精确的 statement，只用了允许的 axioms，并且能被指定的 kernel 接受？
Lean 已经有 kernel，为什么还要再写一个？
答案不是“官方 kernel 不可信，所以换成 nanoda”。nanoda 也有过 soundness bug，而且本系列的主事件正是旧版 nanoda 接受了一个它本应拒绝的 artifact。它的价值来自另一件事：用另一种语言、另一套代码和另一条 proof replay 路径，减少 official Lean kernel 成为唯一故障点。
nanoda 是一个 Rust 编写的 Lean 4 external type checker。
它读取 lean4export 产生的 proof environment，重新检查 declarations、theorem bodies、inductive types、recursors、projections、axioms 和 definitional equality。它不运行 tactic，也不需要相信原项目的 elaborator 输出过程；它关心的是最终导出的 kernel-level 对象能否在自己的实现中成立。
在上一篇 自托管 Dashboard 选型 里，我们把 Glance 归类为“信息聚合型 dashboard”：它既能放服务入口，也能看服务状态、服务器资源、RSS、天气、GitHub release、视频和社区信息。
但选中 Glance 之后，真正的问题才开始：它到底怎么加东西？一个服务应该用哪个 widget？RSS 能不能订阅多个来源？除了官方示例里的天气和 Hacker News，它还能放什么？
这篇就从实际配置出发回答这些问题。