FrenzyMath 宣布完成 Poincaré 猜想 Lean 4 形式化，并通过 Comparator 与双 kernel 检查

FrenzyMath 宣布完成 Poincaré 猜想的 Lean 4 形式化，并称这是其所知首个同时通过完整 Lean build 与 Comparator 验证的版本。当前公开仓库 README 已将项目标记为 complete，记录 Comparator 在指定 commit 上接受公开目标，并由 Nanoda 与 Lean 默认 kernel 检查；团队称数学家与 AI agents 在约半个月内协作完成大部分工作。