Formal Conjectures

在 Lean 中，借助 mathlib 收录的一系列猜想的形式化陈述。

查阅文档：Formal Conjectures 文档

加入我们的 leanprover Zulip 频道

目标

随着包含证明的定理形式化语料库不断壮大，仅有陈述被形式化的开放猜想仍然稀缺。这将在几个方面大有裨益。它可以

成为自动定理证明器和自动形式化工具的优良基准。
借助形式化帮助厘清猜想的精确含义。
通过凸显所需定义，促进 mathlib 的扩展。

我们期待，这一倡议能够孕育出一个更为丰富的形式化猜想数据集。

关于形式化准确性

在没有证明的情况下形式化数学陈述，本身就充满挑战。细微的偏差可能出现，形式化陈述未必能完美捕捉原始猜想的精妙之处。为缓解这一问题，我们将依赖对贡献内容的人工审慎审阅，并计划定期借助 AlphaProof 帮助识别可能的错误形式化。

参与贡献

欢迎贡献——不妨添加你最喜欢的猜想（甚至只需提交一个描述该猜想的 issue）。完整的贡献指南，包括贡献方式、逐步流程、文件结构约定、属性用法以及样式指南，请参阅 CONTRIBUTING.md。

用法、结构与特性

这是一个使用 lake 管理的 Lean 4 项目，并依赖 mathlib。你首先需要安装 elan、lake、lean，如需要还可安装 vscode ，然后再运行

lake exe cache get
lake build

目录结构

目录结构按猜想的来源类型进行组织。有两个特殊目录：

FormalConjecturesUtil 包含诸如 category 属性、answer( ) 展开器以及一些代码检查器。
FormalConjecturesForMathlib 包含潜在适合纳入 mathlib 上游的代码。这里我们遵循 mathlib 的目录结构。

关于本仓库中陈述所使用的 @[category]、@[formal_proof]、@[AMS] 属性以及 answer( ) 展开器的详细信息，请参阅 CONTRIBUTING.md。

版本管理

本仓库将跟踪 mathlib 每月带标签的发布版本（对应 Lean 发布版本），而不是跟踪 mathlib 主分支。

为了减少在添加需要 mathlib 中尚未存在定义的问题陈述时带来的摩擦，这类定义可以添加到 FormalConjecturesForMathlib 目录中。这确保了向 formal-conjectures 添加这些问题时，不受 mathlib 发布节奏的约束。

当 main 分支上的 lean-toolchain 更新时，一个 GitHub Actions 工作流会自动添加形如 v4.{X}.{Y} 的 Git 标签，遵循 mathlib 的标签约定。

稳定的基准快照采用 bench-v{N}-lean4.{X}.{Y} 格式打标签，其中：

v{N}（基准版本）： 标识基准所包含的问题集合。每当问题被添加、移除，或形式化错误得到纠正时，基准版本都会递增。
lean4.{X}.{Y}（Lean 版本）： 标识该快照所使用的 Lean 4 工具链版本。

标签不可变：形式化错误的修复不会修补到现有基准版本中，而是纳入 v{N+1}。

引用 formal-conjectures

如果您的工作使用了 formal-conjectures，请考虑通过以下方式引用它

@misc{FormalConjectures,
  author       = {{The Formal Conjectures Authors}},
  title        = {{T}he {F}ormal {C}onjectures {R}epository},
  year         = {2025},
  url          = {https://github.com/google-deepmind/formal-conjectures},
}

@article{FormalConjecturesPaper,
  authors = {Firsching, Moritz and Lezeau, Paul and Mercuri, Salvatore
    and Horv{\'a}th, Mikl{\'o}s Z and Dillies, Ya{\"e}l and S{\"o}nne, Calle and Wieser, Eric and
    Zhang, Fred and Hubert, Thomas and Ag{\"u}era y Arcas, Blaise and Kohli, Pushmeet},
  title = {{F}ormal {C}onjectures: {A}n {O}pen and {E}volving {B}enchmark for {V}erified {D}iscovery in {M}athematics},
  year = {2026},
  url = {https://arxiv.org/abs/2605.13171v1},
}

许可

其他所有材料均根据 Creative Commons Attribution 4.0 International License（CC-BY）获得许可。您可以在以下地址获取 CC-BY 许可协议的副本： https://creativecommons.org/licenses/by/4.0/legalcode.

相关内容可能基于第三方来源，某些情况下也可能包含第三方内容。每个猜想的原始来源均通过源文件中的 URL 标明。第三方内容可能适用不同的许可要求。具体而言：

来自 Wikipedia 文章、MathOverflow 和 OEIS 的材料，根据 Creative Commons Attribution-Share-Alike License 4.0 发布。
来自 bbchallenge.org 的材料，根据 Creative Commons Attribution 4.0 International License 使用。
来自 Equational Theories Project 的材料，根据 Apache-2.0 使用。
来自 arXiv 的材料，根据源文件中 URL 所示的相关论文适用许可使用。

除非适用法律要求或书面协议另有约定，此处以 Apache 2.0 或 CC-BY 许可协议分发的一切软件及材料，均以 “AS IS”（按原样）方式分发，不附带任何形式的明示或暗示保证或条件。请参阅各许可协议中关于相应权限与限制的具体条款。

这不是 Google 的官方产品。