OpenAI proofdump 把 3SUM 纪录推向 O(n^1.921),Lean 验证通过

iskander · x · 2026-10-16

iskander(Boris Chernyshev 等 AI/算法圈人物)引用一条记录吐槽 OpenAI 的 proofdump 成果:3SUM 问题上界被推向 O(n^1.921),并由 Lean 形式化验证通过(record verified)。

他的观点颇有意味:这些证明会带来「远超人们此前预期的更好的渐近界」,横跨许多基础问题,但可能产不出任何新的可用算法——即理论记录狂飙,实用算法原地踏步。这折射出 AI 辅助数学证明能力与算法设计能力之间的落差。