formal-conjectures 的项目扩展与二次开发

项目的基础介绍

formal-conjectures 是由 Google DeepMind 开源的一个项目，旨在收集和使用 Lean 证明系统对数学猜想进行形式化的陈述。该项目包含了一系列未经证明的数学猜想，旨在为自动化定理证明工具和自动化形式化工具提供基准，同时帮助澄清猜想的精确含义，并促进 mathlib 的扩展。

项目的核心功能

• 收集猜想：项目收集了来自不同来源的数学猜想，包括数学教科书、研究论文、MathOverflow、专门的问题列表等。
• 形式化陈述：使用 Lean 证明系统对数学猜想进行形式化陈述，不包含证明过程。
• 分类与标记：对猜想进行分类（如开放性问题、已解决问题等）并使用 AMS 数学主题分类进行标记。
• 贡献与协作：鼓励社区成员贡献新的猜想形式化、改进现有条目的引用和标签、修复形式化错误等。

项目使用了哪些框架或库？

该项目使用了以下框架和库：

• Lean：一个开源的定理证明系统，用于数学的形式化证明。
• mathlib：一个 Lean 的数学库，为 Lean 提供了广泛的数学理论支持。
• lake：一个 Lean 项目的管理工具，用于 Lean 项目的构建和管理。

项目的代码目录及介绍

项目的代码目录结构如下：

• Util：包含一些实用工具，如分类属性、answer() 轻量级修饰符和一些静态分析工具。
• ForMathlib：包含可能适合合并到 mathlib 的代码，遵循 mathlib 的目录结构。
• 其他目录：按照猜想的来源类型组织，例如来自数学教科书、研究论文等的猜想。

对项目进行扩展或者二次开发的方向

1. 增加新的猜想：继续收集和添加新的数学猜想，特别是那些尚未有形式化陈述的问题。
2. 改进现有形式化：对现有猜想的形式化陈述进行审查和改进，确保其准确性。
3. 扩展功能：开发自动化工具来识别和修复形式化错误，或者增加自动生成猜想形式化陈述的功能。
4. 增强交互性：创建一个交互式界面，允许用户更方便地浏览、贡献和讨论猜想。
5. 集成其他工具：将项目与自动化定理证明工具和其他数学软件进行集成，以促进猜想的证明和验证。
6. 社区建设：建立更活跃的社区，鼓励更多的数学家和计算机科学家参与项目的开发和维护。