Munkres一般拓扑学在Isabelle/HOL中的自动形式化

我们描述一项LLM辅助自动形式化实验，产出了超过85,000行Isabelle/HOL代码，覆盖Munkres拓扑学教材（一般拓扑学，第2-8章）的全部39个小节，内容从拓扑空间一直到维数理论。基于LLM的编码智能体（最初为ChatGPT 5.2，随后为Claude Opus 4.6）为此耗费了24个有效工作日。该形式化是完整的：全部806个形式化结果均被完全证明，零个sorry。已证明的结果包括Tychonoff定理、Baire纲定理、Nagata-Smirnov与Smirnov可度量化定理、Stone-Čech紧化、Ascoli定理、空间填充曲线等。该方法基于“sorry优先”的声明式证明工作流，并结合对sledgehammer的大量使用——这是Isabelle的两大强项。这带来了相对快速的自动形式化进展。我们详细分析了所得的形式化结果，从会话日志中分析了人机交互模式，并与Megalodon、HOL Light和Naproche中的相关自动形式化工作进行了简要比较。结果表明，在Isabelle/HOL中对标准数学教材进行LLM辅助形式化是相当可行、廉价且快速的，尽管一些人类监督仍是有益的。