formal-conjectures 项目亮点解析

项目基础介绍

formal-conjectures 是由 Google DeepMind 开发的一个开源项目，旨在收集并整理数学中已经被形式化但尚未证明的猜想。该项目使用 Lean 编程语言，结合 mathlib 库，为数学猜想提供了一个标准化的形式化表达平台。formal-conjectures 项目的目标是为自动化定理证明工具和自动化形式化工具提供一个优秀的基准，同时通过形式化帮助澄清猜想的精确含义，并促进 mathlib 的扩展。

项目代码目录及介绍

项目的目录结构按照猜想的来源类型进行组织。以下是一些主要目录的介绍：

• Util: 包含一些工具，例如用于标记问题类别的 category 属性、answer() 调用器以及一些静态分析工具。
• ForMathlib: 包含可能适合上传到 mathlib 的代码，遵循 mathlib 的目录结构。
• 其他目录: 按照猜想的来源，如数学教材、研究论文、MathOverflow 问题等，分别存放不同的猜想形式化描述。

项目亮点功能拆解

1. 分类属性: 每个猜想都可以通过 category 属性进行分类，区分开开放性问题、已解决问题、研究生/本科生/高中生级别问题等。
2. AMS 标签: 使用 AMS MSC2020 标准的主题分类，方便用户了解每个猜想与哪些数学领域相关。
3. answer() 调用器: 对于一些需要用户给出答案的问题，如 Hadwiger–Nelson 问题，answer() 调用器允许用户在不知道答案的情况下形式化问题。

项目主要技术亮点拆解

1. 基于 Lean 编程语言: Lean 是一个高效的定理证明系统，formal-conjectures 利用 Lean 的强大功能，为数学猜想的形式化提供了坚实的基础。
2. 集成 mathlib 库: mathlib 是 Lean 的一个大型数学库，formal-conjectures 的集成使得可以利用已有的数学定义和定理。
3. 严谨的代码审查: 项目鼓励贡献者通过 pull request 提交猜想的形式化描述，每个提交都会经过严格的代码审查，确保猜想的准确性和形式化的正确性。

与同类项目对比的亮点

相比其他收集数学猜想的项目，formal-conjectures 的亮点在于其形式化的严谨性和与 Lean 社区的紧密集成。它不仅收集猜想，还鼓励社区成员参与到形式化的过程中，通过严格的审查流程保证猜想的质量。此外，项目通过分类和标签功能，提供了更细粒度的搜索和浏览能力，有助于研究者和开发者快速找到感兴趣的猜想。