前Intel工程师给AI狂热泼冷水：解出数学难题，不等于能替代白领

OpenAI 9/9公开Navier-Stokes证明：约1万个Agent协同88小时求解，Astra再用17小时完成Lean机器验证。前Intel工程师Jay Kruer指出，数学有明确答案且Lean可自动裁判；现实编程、研究和企业任务目标模糊，无程序判定对错，规则写严又依赖昂贵领域专家，监督验收成本可能高于人自己完成。其CPU形式化验证背景，点出瓶颈已从解题能力移到可验证性。

OpenAI 9/7披露，8月中旬人类每工作8小时，多Agent合计运行约24.8小时，折算3.1个Agent工作日。Agent吞吐在涨，白领替代仍卡在缺少Lean式自动验收；没有可靠裁判，人必须持续盯盘，Kruer的“开挂实习生”仍难升级为管理者。