MathCode: 为终端编码智能体引入 Lean 4 形式化引擎

AI 导读

这是一个开放工具与工作流原型，不代表自主定理证明已经解决。项目页把 MathCode 标为 2026 年 4 月项目，当前列出的最新版本 v0.2.0 发布于 5 月 26 日；这里列在 8 月 16 日，是因为 Hacker News 讨论让它重新进入公共视野。最值得关注的是围绕 Lean 形成紧密的“编写—编译—诊断”闭环；已核验的项目页面没有给出证明成功率、基准对比，仓库也未显示明确许可证。