Munkres 《一般拓扑学》在 Isabelle/HOL 中的自动形式化
人工智能
2026-04-10 v1 机器学习
计算机科学中的逻辑
摘要
我们描述了一项由 LLM 辅助的自动形式化实验，产生了超过 85000 行的 Isabelle/HOL 代码，覆盖 Munkres 《拓扑学》（一般拓扑学，第 2--8 章）的全部 39 节内容，从拓扑空间到维数理论。该实验最初使用 ChatGPT 5.2 然后改用 Claude Opus 4.6，耗时 24 个活跃天。该形式化是完整的：所有 806 个形式化结果都经过完全证明，没有一个 "sorry"。已证明的结果包括 Tychonoff 定理、Baire 类别定理、Nagata-Smirnov 和 Smirnov 度量化定理、Stone-Čech 紧化、Ascoli 定理、空间填充曲线等。该方法基于 "sorry-first" 声明式证明工作流程，结合大量使用 sledgehammer——这两者都是 Isabelle 的主要优势之一。这导致相对快速的自动形式化进展。我们详细分析了所得形式化，分析了人类与 LLM 交互模式（来自会话日志），并简要与 Megalodon、HOL Light 和 Naproche 等相关自动形式化工作进行了比较。结果表明，LLM 辅助在 Isabelle/HOL 中对标准数学教科书进行形式化是相当可行的、廉价且快速的，即便某些人类监督也有用。
引用
@article{arxiv.2604.07455,
title = {Munkres' General Topology Autoformalized in Isabelle/HOL},
author = {Dustin Bryant and Jonathan Julián Huerta y Munive and Cezary Kaliszyk and Josef Urban},
journal= {arXiv preprint arXiv:2604.07455},
year = {2026}
}