我们做 ChatBlog，是因为经常需要临时弄懂一个东西。
可能是一个新概念，也可能是一项工具、一篇论文，或者一个需要尽快拿出方案的问题。调研结束后，资料散在链接、聊天和笔记里，下一次再遇到，往往还得重新翻找。ChatBlog 想把这些过程留下来：把零散信息整理成可以看懂的内容，帮助我们消化，也方便以后找到、继续使用。
AI 让这件事有机会做得更快。查找、整理、解释和制作页面的成本降低了，一次临时探索也能留下一个可阅读的结果。但文章生成得快，不代表知识已经被理解。我们真正需要的是有人看完以后，能比之前更清楚一点。
想用一个低延迟模型玩游戏，最省事的起点是找一套已经能运行、还能看清决策过程的项目。画面动起来只是第一步：还要知道模型看到了什么、返回了什么，以及代码有没有替它改动作。
这次筛选了十个现成项目，重点读了三套实现：PlayJev、本地 Laya 与 Jev 的对战 Arena，以及社区 Playground 里的 MicroDuck。它们分别代表画面输入、游戏状态输入和传感器输入三条路线。本文整理源码与启动方式，没有把作者报告的速度和得分当作自己的复现实测。
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 社区或本文的共同结论。
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 接受？