Djalil Chafaï 用 ChatGPT Codex + agents 在约 6 小时内完成论文 Theorem 1.9 的 Lean 形式化

数学家 Djalil Chafaï 报告使用 ChatGPT Codex CLI（5.6 Sol）和 agents，将其最新论文 arXiv:2608.19358v2 的 Theorem 1.9 自动形式化为约 16,400 行 Lean、约 75 个文件。整个过程在个人 Debian 工作站上耗时约 5 小时 48 分钟、使用约 806 万 tokens；最终 full make 成功，没有 sorry、admit、sorryAx 或 project axioms，主定理仅依赖 Mathlib 标准公理。