FrenzyMath 报告该项目约包含 320 万行 Lean，LLM 与计算服务器总成本低于 3 万美元。 仓库将仅依赖 Mathlib 的 endpoint statements 与证明库分离，并保存 Comparator 配置、 verifier 版本、日志和源码 provenance 记录。
2026 年 9 月 28 日，FrenzyMath 宣布完成三维 smooth 与 topological 庞加莱猜想的 Lean 4 形式化，证明路线主要跟随 Morgan–Tian 对 Hamilton–Perelman 证明的阐释。 团队报告全量 Lean build 已通过，并使用 Comparator 对两个公开 endpoint statement 进行验证，同时由 Lean kernel 与 Nanoda 检查，允许的公理仅为 propext、 Classical.choice 与 Quot.sound。FrenzyMath 表示，三名具有数学背景的 AI 开发者与 数名志愿数学家使用公开商用 LLM，在约半个月内完成了大部分工作。
FrenzyMath 报告该项目约包含 320 万行 Lean，LLM 与计算服务器总成本低于 3 万美元。 仓库将仅依赖 Mathlib 的 endpoint statements 与证明库分离，并保存 Comparator 配置、 verifier 版本、日志和源码 provenance 记录。公告同时指出，Ziyang Qin、Yuan Liao、 Ayush Khaitan 与 Bennett Chow 等组成的独立团队在同一天稍早也发布了另一套完整 庞加莱 Lean 开发；该独立 arXiv 论文记录了公开全量构建，并说明证明与文字工作中使用了 自动化辅助。
庞加莱猜想是现代数学的基础性定理，其标准证明依赖庞大的几何分析、拓扑、偏微分方程与 Ricci flow 理论体系。把这种规模的项目压缩到数周 AI 辅助形式化，说明前沿形式数学 Agent 已能处理广泛前置理论库，而不再局限于孤立奥赛定理或短篇研究论证。近乎同期出现的第二套 独立形式化进一步强化了这一历史信号，同时也提醒 Chronicle 不应把里程碑简单归为单一项目 的优先权。
重要性说明：FrenzyMath 的庞加莱猜想形式化构成 AI 辅助形式化方向的领域级里程碑：该项目把完整的 smooth/topological Poincaré 证明路线组织成数百万行 Lean 工程，并报告主要工作在约 半个月内通过 agentic pipelines 与公开商用大语言模型完成。项目公开了面向 Mathlib 的独立 statement、全量构建证据以及 Comparator/Nanoda 验证。几乎同期，另一支团队 也发布了独立完整 Lean 开发，表明研究级几何分析形式化已经从孤立演示走向可重复的 前沿实践。由于数学定理本身早已解决，且逐定理的人机分工并未被完整重建，因此 H2 比 H1 更合适。
FrenzyMath 的公告与公开仓库提供 endpoint statements、证明库、全量构建说明以及 Comparator/Nanoda 验证记录。本轮 Chronicle 没有自行独立重放该 artifact，因此 machine_checked 表示公开的机器检查证据，而不是 independently_replayed 状态。
当前没有记录的更正。
