陶哲轩12年前预言“未来可用形式化语言写论文”被视为天方夜谭，如今他亲证Lean4与Copilot揪出论文错误，并预言AI将在10年内独立提出数学猜想甚至获得菲尔兹奖。
陶哲轩主导的First Proof二期评测结果揭晓，AI系统以最低8美元一道题的成本，成功解出7道达到论文发表标准的世界级数学难题。
