其实astra最牛的地方是这张图。

这张图的“赛场”不是普通数学题，而是一个含68道未解开放问题的Erdős精选难题库——全是数学家们几十年没啃动的硬骨头。Astra拿了3%，换算过来就是在有限时间+有限算力预算下，成功证明了其中2道。其他所有顶级模型，一道都做不出来，全部零分。

如果不限时间、不限算力，Astra能解决5道。这5道，全人类至今无解。

3%看似微薄，但请想清楚——其他模型的0%，意味着它们连“碰”一下这些问题的资格都没有。而Astra的3%不是选择题蒙对的，是实实在在的Lean形式化证明，每一步推理都可被机器验证。限时只能拿下2道，放开资源就能多拿3道，这说明它的推理能力是“真家伙”，只是受限于搜索深度和计算量，而不是模型本身在猜。

数学史上，从“0”到“1”的突破永远比从“1”到“100”更难。Astra这3%就是那个“1”——第一个能自动发现人类未解定理的AI。其他模型再大、再贵，在这个硬核擂台上都是白纸一张。

所以别嘲笑这个百分比。它宣告的不是“AI还不行”，而是“AI终于摸到了人类智力天花板的那条缝”。一旦这条缝被撬开，以后我们可以用成千上万的并行证明器去撞击那些悬赏百年的难题，每撞出一份Lean证明，就是一块新的数学基石。

硬核推理，永远是智能的终极考场。而Astra，是第一个交卷的AI，哪怕只写了第一道大题的前两行。（by AI）

资料：Erdős问题总数约为1217–1220题已解决（proved / disproved / otherwise solved）约一半左右（官网显示约584题已解决，占比约48%）。完全开放（open）的约590–650题。====FrontierMath Erdős：这是Epoch AI于2026年推出的FrontierMath Erdős（FME）基准，专门针对大语言模型/AI系统的研究级数学能力测试。精选68道（覆盖约65个编号问题，部分问题拆成多个Lean猜想，如Hadwiger–Nelson问题拆成3个）。由Thomas Bloom从当时约650道未解问题中亲自挑选，约占当时未解问题的10%。全部在2026年8月时仍为开放问题。

挑选标准：Bloom认为数学上重要且困难的“喜爱问题”，而非随便挑的简单题。全部用Lean 4（配合Mathlib）形式化陈述。AI必须自主写出完整的Lean证明或反证，并通过形式验证才算解决。约50条来自Google DeepMind的Formal Conjectures库，其余由团队自动形式化后经Bloom人工审核。

评测规则：严格控制预算与时间（默认每题300美元 + 72小时工作时间），单次尝试。强调自主性、可复现性和形式正确性，避免“搜到旧文献就算解决”的水分。