标签
OpenFrontiers 推出了一个跨学科语料库，包含 12,151 个尚未解决的研究问题，以及一个由 200 个近期已解决的数学问题组成的回溯性基准，这些问题均附有 Lean 4 形式化陈述。该研究评估了七个大语言模型智能体，发现它们在闭卷条件下重新发现研究级成果的情况仍然罕见，而在实时联网条件下取得的成功则主要源于检索已发表的解答。