形式猜想：数学验证发现的开放且不断发展的基准

随着自动推理系统的快速发展，越来越需要研究级的形式数学问题来准确评估其能力。为了解决这个问题，我们提出了形式猜想，这是精益 4 中形式化的当前 2615 个数学问题陈述的不断发展的基准。该数据集源自活跃的数学研究领域，具有 1029 个开放研究猜想，为数学证明发现提供了零污染基准，并解决了 836 个证明自动形式化问题。值得注意的是，该存储库提供了一个结构化接口，将数学家与人工智能系统和试图解决这些问题的人类联系起来，数学家形式化并澄清了问题。该基准展示了其直接效用，已被用来做出新的数学发现，包括解决开放研究猜想。我们描述了在协作开源项目中确保这些形式化的正确性的方法，该项目的贡献来自活跃的社区。在这个框架中，人工智能生成的证明和反证作为一种有价值的审计机制，可以迭代地提高基准的保真度。最后，我们提供了标准化的评估设置并报告了冻结评估子集的基线结果，展示了可攀登的信号，可测量研究级数学自动推理的当前前沿。