vltanh/formalize-math-paper

在Lean 4中形式化数学论文

您交付一个Lean项目，其中包含相关文档：

• 论文证明的每个结果都由论文自身的论证证明。只有在必要时才偏离论文的证明，并且每次偏离都会被报告（规则，“忠实证明”）；
• 论文在证明中引用的每个结果也都被证明：在Mathlib中、在其他公共库中、或在External/中。被引用的结果可能需要某种Lean库尚没有、并且项目无法合理构建的数学知识。这样的结果将成为每个使用它的语句的命名假设，形式化将明确说明这是有条件的；
• 语句与论文陈述一致，任何偏差都有文档记录；
• lake build成功，没有sorry（Challenge.lean中的语句除外，这是设计使然）、没有admit，也没有项目axiom。库中的每个声明仅依赖于propext、Classical.choice和Quot.sound；
• REPORT.md对论文进行形式化审计。它以接下来的工作结尾：自论文发表以来该主题的发展情况、其结果如何被扩展、推广或加强，以及其证明如何能够更简洁。README.md总结形式化工作，CREDITS.md说明其制作过程：步骤、使用的代理和模型、时间和精力（运行日志）；
• 一份私有的NEXT.md，除非用户要求，否则绝不发布，它回答了用户接下来可以写什么论文：几个候选主题，每个都可以成为一篇独立的论文，并进行深入探讨（障碍、尝试、证据、已证明的内容），而不是一份增量扩展的列表；
• 该项目已为Palomar打包，并在用户许可下发布并通过Palomar的预检。

工作分为两个阶段。在第1阶段，形式化论文本身证明的所有内容。论文从文献中取得的结果可以是临时公理。在第2阶段，消除这些公理：证明它们，或者将触及不到的结果转化为明确的假设。准备工作在两个阶段之前，而验证、清理、审计和打包则在之后。

原则

这些原则解释了下面的规则。当没有规则涵盖某种情况时，使用它们。

• 论文是陈述和论证的真理来源；Lean判断正确性。 与论文不同的陈述，无论其证明多么简洁，都是错误的形式化。同样，通过另一种论证得出论文陈述的证明也是如此：形式化检查的是论文的证明，而不仅仅是它的主张。在任何人证明之前，对照TeX源审查陈述。一旦证明被写出来，就将它们与论文的证明进行比较。永远不要悄无声息地更改其中任何一个。
• 没有人编译过的形式化是一个草稿。 凭记忆编写且从未编译的Lean通常包含猜测的引理名字、错误的签名和虚假的辅助引理。当Lean工具链可用时，进行编译。如果没有，或者用户禁止编译，要明确说明结果是未经验证的。
• “标准的”、“显然的”、“由对称性”、“例行的”仍然需要证明。 Mathlib可能已经有这个事实；如果没有，就证明它。只有论文本身从其他来源取得的内容才可能成为公理。
• External 表示结果的来源，并不意味着它被信任。 被引用的结果存在于External/中是因为它的来源。它像其他所有内容一样需要被证明。
• 假设就是假设，无论其形式如何。 一个未被证明的引用结果就是被假定的，无论它是作为公理、假设还是结构的一个字段写入。不允许有公理。当语句的读者能够看到每个假设时，允许有假设，并以它所假设的结果命名。将数据与假定定理混合在一起的结构会隐藏结果依赖的内容。同样，一个类型看起来像数据但包含定理的参数也会隐藏依赖关系。
• 数据伴随着其定义性质。 当一个语句将一个论文中的对象作为参数而不是构造它时，它还必须要求定义该对象的性质。否则，该定理是关于满足其他假设的每个对象的，这是一个不同的陈述。
• 表示选择需要桥梁。 Lean中的对象可能与论文中的不同：从0而不是1开始的索引、列表而不是索引族、绑定在一起的Mathlib结构而不是非正式的对象、具体的模型而不是“同构意义下”的描述。当出现这种情况时，证明一个连接两者的引理，并记录这个选择。永远不要假设两个表示是等价的。
• 常量和范围是数学的一部分。 幂、因子、天花板、地板、严格不等式与弱不等式、范围的端点以及ℕ上的截断减法决定了语句的真假。
• 诚实报告。 如果某一步被跳过、证明失败、语句必须更改、或者证明不得不偏离论文，要说明原因。审计只有在可信任的情况下才有用。
• 证明中的空白不是一个错误的语句。 当论文的证明使用了其假设未提供的事实时，该语句可能仍然为真。在你对语句下任何结论之前，先寻找一个正确的论证。
• 衡量工作。 读者和注册表会询问形式化是如何完成的。边做边记录答案成本很低，而事后重建则很困难。

规则

• 永远不要为了证明成立而削弱或改变论文结果的陈述。 如果论文的陈述是错误的，立即停止处理它并告知用户，同时给出反例。同时，其他工作可以继续。如果用户同意，形式化最近似的正确版本，并在报告中将其记录为一个错误。明显的印刷错误是唯一的例外（见下文）。

• 永远不要仅仅因为结果证明似乎需要某个假设而将其添加到论文结果中。 添加一个假设会削弱结果。只有当语句本身有反例时才添加假设，而不是因为证明中的某一步失败，然后遵循上一条规则。否则，通过修正后的论证证明原样陈述的语句，并将证明中的空白记录为一个E项。如果你既找不到证明也找不到反例，请告知用户缺少什么。由他们决定是继续工作还是形式化一个更弱的、有文档记录的偏差版本。

• 忠实证明。 通过论文的证明来证明每个结果：相同的中级主张、相同的构造和情况划分、以及论文引用相同的前述结果。论文证明所引用的结果构成了它的路线。形式化证明必须具有相同的路线，而路线检查（第6阶段）会验证这一点。只有机制可以不同：策略、闭合一个常规步骤的Mathlib引理、独立步骤的顺序，以及封装论文中某一步骤的辅助引理。如果Mathlib恰好证明了一个编号的结果，仍然要用论文的论证来证明它，除非论文本身将其视为已知（它引用了它，或者称之为标准）。

• 只有在必须时才偏离论文的证明，即出于以下原因且无其他原因：

  1. 论文的论证在该步骤是错误的，或者那里有空白，并且无法沿着它自己的思路修复（该步骤也是一个E项）；
  2. 该步骤需要Lean缺少且项目无法合理构建的数学知识（如同无法触及的引用结果，见下文），而另一种论证则避免了它；
  3. 该步骤在形式化必须使用的表示中没有意义（原则），因此对其的忠实翻译是一个不同的论证。

  更短、更优雅、更通用或更自动化的证明都不是理由。更容易形式化或构建更快的证明也不是。你发现的更简单的论证仍然值得保留：记录下来，附上草图，用于报告的“接下来做什么”部分（第8阶段），然后用论文的论证来证明结果。偏离的程度以原因要求为限：修复该步骤，而不是证明。如果某个偏离会替换整个编号结果的论证，而不仅仅是某一步，请先向用户提出建议，并说明原因。同时，其他工作继续。

• 永远报告每次偏离。 对于每一次偏离，记录论文做了什么，形式化做了什么替代，以及哪个原因迫使了更改。在声明的文档字符串（“偏离论文：…”）、报告的偏离表格、formalization.yaml（fidelity.divergences）、任何伴随文本、路线检查的已记录差异文件（当路线改变时）以及下一次状态报告中记录它。任何一份文件中缺失的偏离都是一个缺陷：找到并修复它，就像修复一个被悄无声息更改的语句一样。

• 无法触及的引用结果。 被引用的结果可能需要某个Lean库尚没有的数学知识。如果在项目中构建该数学知识是中等努力，那么就构建它。否则，默认做法是有条件的形式化：该结果成为每个在其证明中使用它的语句的命名假设。不经询问就应用默认做法，并在下一次状态报告中报告。仅当构建缺失的数学知识是一项庞大但可行的工作时才询问用户：是否花费该努力由他们决定。同时，在默认做法下继续其他工作。如果他们选择构建，就按层次规划工作。每一层用更基础的内容的构造和证明替换一些假设，并结束于一个可发布的状态。这些假设是唯一可以添加到没有反例的论文结果中的假设。永远不要将有条件的形式化呈现为完整的：其README、formalization.yaml和报告要说明它是有条件的，并列出它所假设的内容。

• 语句中的错误。 如果一个语句仅因为一个明显的印刷错误（错误的索引、交换的名字、缺少- 1）而错误，并且只能有一种解读，那么立即在库和Challenge中形式化该解读。在报告中以及下一次向用户的状态报告中列出每个这样的修正。当可能的修正不止一个时，将该语句视为错误的。

• 一个错误的辅助引理（你或草稿引入的）需要具体的反例，并尽可能在Lean中进行检查（decide、norm_num或#eval）。然后添加最小的假设，更新其调用者，并在提交消息中记录更改。

• 最后没有sorry（Challenge.lean之外）、admit、axiom、native_decide或implemented_by。 native_decide添加了一个公理，Comparator会拒绝它。

• 永远不要猜测Mathlib的名字或签名。 在.lake/packages/mathlib中固定的源文件里搜索，或使用#check、exact?和Loogle。Mathlib经常重命名和弃用声明，弃用警告会命名替代品。

• 如果你无法编译（没有工具链，或者用户禁止），不编译直接编写Lean。对照固定的Mathlib源文件检查每个名字、签名和导入路径，保持语句优先的顺序，并将每个结果标记为未经验证。以后编译项目的人从第3阶段开始。

• 每次检出只运行一个lake build。 同时运行的构建会互相删除对方的.olean文件，而在项目上打开的编辑器会运行自己的lake setup-file构建。如果你看到“object file … does not exist”，请重试，而不是通过编辑绕开它。

• 在任何他人可见的操作前征求许可： 推送、创建仓库、更改仓库可见性、打开或关闭拉取请求、删除分支、运行Palomar的预检、提交到Palomar、注册。对其中一项的许可不等于对其他项的许可。

• 作者是人。 在README、CREDITS.md和formalization.yaml的automation部分中注明AI系统的贡献，但绝不要将其列为作者或维护者。

• 从一开始就保留运行日志（见下方“运行日志”）。在CREDITS.md、formalization.yaml和状态报告中报告它。

工作流

阶段	目标	完成标志
0. 配置	记录任务，提出未解决问题	配置已记录
1. 盘点	了解论文：其结果、定义、常量、引用及其证明来源、疑似印刷错误	工作清单完成
2. 项目	基于Mathlib版本的Lean项目，包含模块系统，按论文章节布局	lake build运行成功
3. 语句	陈述每个定义和编号结果，并包含sorry证明；Challenge	语句细节化并通过独立审核（对照论文）；基准线已提交
4. 第1阶段	用论文的证明证明论文证明的所有内容	只剩下被引用的结果，作为External/中的公理；所有偏离已报告
5. 第2阶段	证明被引用的结果	零公理；每个仍被假设的结果都是命名假设
6. 验证	公理审计、依赖表、路线检查、解决方案和Comparator	scripts/Audit.lean和路线检查通过；证明与论文的证明进行比较；Comparator接受
7. 清理	无警告、无未使用的假设、无误导性名称、路线未变	构建只显示Challenge的sorry；路线检查仍然通过
8. 审计	REPORT.md、README.md、CREDITS.md；私有NEXT.md	每个发现都对照TeX源进行检查；每个后续候选主题都检查其新颖性并符合标准
9. 打包	CI、Palomar文件和检查；发布和预检，经许可	Palomar的本地检查通过；发布后，预检报告status: pass

在每个里程碑处提交，提交消息说明更改了什么以及为什么。

第0阶段：配置

记录以下内容。只询问你自己无法解决的事项：

论文：            arXiv ID和版本（或DOI）；如有，提供源TeX；后续版本

…