用大模型辅助形式化拓扑学经典教材，零遗憾证明806个定理。
Munkres' General Topology Autoformalized in Isabelle/HOL
- 先写'抱歉'再补证，结合Isabelle强大工具批量生成证明
- 24天完成39章内容，806个定理全部严格证明无遗漏
- 适合数学形式化研究者与对自动化证明感兴趣的开发者
我们描述了一项基于大模型辅助的形式化实验，生成了超过85,000行Isabelle/HOL代码，覆盖了Munkres《拓扑学》（一般拓扑，第2–8章）的全部39个章节，从拓扑空间到维数理论。该过程耗时24天，使用ChatGPT 5.2和Claude Opus 4.6作为编码代理。形式化结果完整：所有806个正式命题均被完全证明，未留下任何'sorry'。已证明的定理包括蒂霍诺夫定理、贝尔范畴定理、纳加塔-斯米尔诺夫与斯米尔诺夫度量定理、斯通-切赫紧化、阿斯科利定理、空间填充曲线等。方法基于“先抱歉”声明式证明流程，并大量使用sledgehammer工具——Isabelle的两大优势。该方法显著加快了自动形式化进度。我们详细分析了形式化成果及会话日志中的人机交互模式，并与Megalodon、HOL Light、Naproche等系统进行了简要比较。结果表明，在Isabelle/HOL中利用大模型辅助形式化标准数学教材是可行、经济且快速的，尽管仍需一定人工监督。
原文摘要 · Abstract (English)
We describe an experiment in LLM-assisted autoformalization that produced over 85,000 lines of Isabelle/HOL code covering all 39 sections of Munkres' Topology (general topology, Chapters 2--8), from topological spaces through dimension theory. The LLM-based coding agents (initially ChatGPT 5.2 and then Claude Opus 4.6) used 24 active days for that. The formalization is complete: all 806 formal results are fully proved with zero sorry's. Proved results include the Tychonoff theorem, the Baire category theorem, the Nagata--Smirnov and Smirnov metrization theorems, the Stone--Čech compactification, Ascoli's theorem, the space-filling curve, and others. The methodology is based on a "sorry-first" declarative proof workflow combined with bulk use of sledgehammer - two of Isabelle major strengths. This leads to relatively fast autoformalization progress. We analyze the resulting formalization in detail, analyze the human--LLM interaction patterns from the session log, and briefly compare with related autoformalization efforts in Megalodon, HOL Light, and Naproche. The results indicate that LLM-assisted formalization of standard mathematical textbooks in Isabelle/HOL is quite feasible, cheap and fast, even if some human supervision is useful.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。