Astra 宣称解决五个开放 Erdős 问题，并行烧算力做数学成新范式

BLUECOW009 · x · 2026-09-04

tmkadamcz 称 Astra 解决了五个开放 Erdős 问题（#1、#74、#126、#548、#571），并表示这是他首次发现一类可以「每小时人类工作配数百万美元算力」还划算的任务。其构成条件：1) 结果可形式化验证（Lean 证明）；2) 验证过的结果本身对数学家有价值；3) AI 现在已能部分成功。可以同时跑数千个并行证明实例数周，只在真正产出 Lean 证明时才看输出——这和编码智能体的用法截然不同。作者认为这种「能无限堆算力」的特性可能是件大事。