Flyspeck 项目教程

1. 项目的目录结构及介绍

Flyspeck 项目的目录结构如下：

flyspeck/
├── azure/
├── formal_graph/
├── formal_ineqs/
├── formal_lp/
├── informal_code/
├── jHOLLight/
├── kepler_tex/
├── legacy/
├── text_formalization/
│   └── build/
│       └── ocamlinit_hol_light.ml
├── usr/
├── .gitattributes
├── .gitignore
├── INSTALL.md
├── LICENSE
├── README.md
└── load_flyspeck.ml

目录结构介绍

• azure/: 文件相关于非线性不等式的形式验证。这些不等式首先通过在 Microsoft Azure 云上的计算进行形式验证。
• formal_graph/: 文件相关于在 Isabelle 证明助手中的驯服图分类的形式验证。大多数这些文件是 Isabelle 形式证明档案的一部分，应从该档案下载代码。
• formal_ineqs/: 文件相关于非线性不等式的形式验证。
• formal_lp/: 文件相关于线性程序的形式验证。
• informal_code/: 用于 Kepler 猜想证明的非形式化计算机程序代码。这些文件不是 Flyspeck 项目所必需的。
• jHOLLight/: 用于 Solovyev 的 SSReflect 模式的 Java 前端代码。
• kepler_tex/: 书籍 "Dense Sphere Packings" 的 LaTeX 源文件。
• legacy/: 包含不再使用的死代码。可以忽略此目录。
• text_formalization/: 项目的主要目录，包含文本部分的形式化文件，如书籍 "Dense Sphere Packings" 中所述。
  • build/: 包含与构建项目相关的文件。
    • ocamlinit_hol_light.ml: 主要用于构建项目的文件。
• usr/: 这些文件不是 Flyspeck 项目的一部分，主要包含 Hales 撰写的文章的 LaTeX 文件。

2. 项目的启动文件介绍

Flyspeck 项目的主要启动文件是 load_flyspeck.ml。该文件用于加载和初始化项目所需的所有模块和依赖项。

启动文件介绍

• load_flyspeck.ml: 该文件是项目的入口点，负责加载所有必要的模块和配置，以便项目能够正常运行。

3. 项目的配置文件介绍

Flyspeck 项目的主要配置文件是 INSTALL.md 和 README.md。

配置文件介绍

• INSTALL.md: 提供了项目的安装指南，包括详细的步骤和依赖项说明。
• README.md: 提供了项目的概述、安装指南、资源链接以及项目的许可证信息。

通过这些文件，用户可以了解如何安装和配置 Flyspeck 项目，以便进行进一步的开发和研究。