标题：陶哲轩转发！DeepMind开源「AI数学证明标准习题集」

DeepMind最新开源了形式化数学猜想库，这一资源集合了经典数学猜想的形式化表述，如解析数论中的朗道问题。此外，库中提供代码函数，便于将自然语言的数学猜想转化为形式化表述。

陶哲轩曾利用Lean工具形式化证明PFR猜想，其第一步正是将猜想核心概念转为计算机可验证的形式化版本。对此，陶哲轩转发并评价：“对开放性问题进行形式化表述是利用自动化工具的重要一步。”

该猜想库由DeepMind建立后，鼓励所有人添加数学猜想，呼吁全球数学家积极参与。资源不仅有助于自动定理证明工具的测试，还能提升AI数学推理能力。其内容涵盖多种类型数学猜想，并支持随时扩展与审核。

通过添加新问题、提出建议、修正错误等方式，用户可参与建设。具体操作需在GitHub上创建问题、fork仓库、按结构添加猜想，并通过本地构建命令检查后提交拉取请求。库中内容经人工审核与AlphaProof辅助识别，确保准确性。

DeepMind与陶哲轩的合作频繁，陶哲轩曾高度评价DeepMind的FunSearch方法，称其为数学发现的创新范式。近期，双方合作推出的AlphaEvolve在多个数学领域取得突破，展现了AI与数学结合的巨大潜力。

形式化数学猜想库链接：https://google-deepmind.github.io/formal-conjectures/
项目地址：https://github.com/google-deepmind/formal-conjectures
参考链接：https://mathstodon.xyz/@tao/