随着通用人工智能向硬核科学研究领域渗透，AI数学推理能力、形式化验证技术的落地需求正在持续攀升：前者被视为通用智能的核心评价标尺之一，后者则是高端芯片设计、航空航天控制系统、高风险医疗软件等领域保障产品安全性的核心技术，但长期以来，该领域的研究始终面临基准数据集存在数据泄露、评估标准不透明、推理场景过度简化等共性痛点，直接制约了技术迭代效率。
2026年5月13日，谷歌DeepMind联合相关机构正式发布动态演进的形式化数学基准数据集Formal Conjectures，相关成果首发于预印本平台arXiv，旨在为全球自动化推理系统提供研究级数学问题的精准评估依据。
据公开信息显示，该数据集共包含2615条使用Lean 4形式化的数学命题，其中1029个为未被公开证明的开放猜想，可实现零污染的证明发现能力评估，彻底避免训练数据提前包含答案导致的评估失真问题；另有836个已解决问题，可用于自动形式化验证算法的效果测试。所有数据均源自Erdős问题集、维基百科数学词条、顶级数学学术论文、MathOverflow社区讨论等多个活跃数学研究领域的权威资料库，覆盖代数、数论、组合数学等多个细分研究方向。为保障数据的高保真度，该数据集的构建采用协作式开源管道，通过三级误形式化分类法对命题的形式化准确性进行多轮校验，同时创新性引入了answer(sorry)机制，将答案发现与证明验证两个环节完全分离，进一步提升了评估体系的科学性。
从潜在应用场景来看，该数据集首先可直接服务于人工智能驱动的数学定理自动证明研究，科研团队可依托零污染的开放猜想集测试大模型的原创数学推理能力，推动AI辅助数学研究的落地；其次在工业级形式化验证领域，该数据集的高难度、高保真命题可用于打磨芯片功能验证、高安全等级软件正确性验证的算法模型，降低高端制造领域的验证成本；此外，该数据集的开源协作构建模式，也可为后续专业科研数据集的标准化生产提供参考。
目前，该数据集已面向全球科研团队开放使用，将有效填补自动化推理领域优质基准的空白，推动研究级数学的自动化推理前沿技术迭代，同时也为科研类数据要素的高价值转化提供了典型样本。
详情页内容：
_1769672084863.jpg)