LeanEuclid 的项目扩展与二次开发

项目的基础介绍

LeanEuclid 是一个面向欧几里得几何自动化形式化的开源项目，旨在通过 Lean 证明助手对欧几里得几何问题进行形式化表示和证明。该项目基于 Lean 4 编程语言，利用 SMT（Saturation-Matching-Theorem）求解器来自动进行图示推理，为机器学习在几何证明领域的应用提供了基础。

项目的核心功能

• 形式化系统 E 的实现：LeanEuclid 在 Lean 中实现了形式化系统 E，用于忠实地形式化 Euclid's Elements 中的证明，包括图示推理。
• 定理和证明的自动化：项目提供了 173 个欧几里得几何问题的手动形式化 Lean 代码，这些问题包括来自 Euclid's Elements 的 48 个问题和基于 UniGeo 数据集的 125 个问题。
• 证明等价性检查：通过 E3 工具，项目能够执行标准及近似等价性检查，以评估自动形式化的定理陈述与真实定理陈述的一致性。

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

• Lean 4：一个基于定理证明的编程语言，用于开发 LeanEuclid 的核心逻辑和证明系统。
• SMT 求解器：如 Z3 和 CVC5，用于 Lean 中的自动图示推理。
• Python：用于项目中的服务器环境路径设置和本地文档服务。

项目的代码目录及介绍

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

• Book：包含 Euclid's Elements 中第一卷的形式化定理和证明。
• UniGeo：包含基于 UniGeo 数据集的问题的形式化定理和证明。
• E3：实现定理陈述等价性检查的代码。
• images：存放项目相关的图像文件。
• scripts：包含项目构建和开发相关的脚本文件。
• .dockerignore、.gitignore、Dockerfile：包含 Docker 相关的配置文件。
• lakefile.lean：Lean 的项目构建配置文件。
• lean-toolchain：Lean 工具链的配置文件。

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

• 增加新的几何问题：可以向项目添加更多的欧几里得几何问题，以扩展测试和评估的覆盖范围。
• 改进自动化推理算法：通过优化 SMT 求解器的使用或开发新的推理算法，提高自动化形式化和证明的效率。
• 增强图形用户界面：开发一个图形用户界面，以便用户更直观地与 LeanEuclid 交互。
• 集成其他数学库和工具：将 LeanEuclid 与其他数学软件和库集成，如数学符号识别库，以拓宽应用场景。
• 多语言支持：考虑为 LeanEuclid 添加其他语言的支持，以便更多的用户能够使用和贡献。