130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?

这是一个简要介绍，描述了一个已将Munkres拓扑学教材中大量内容自动形式化的项目（该教材共7章39节，总计241页）。该项目自2025年11月21日启动以来，截至2026年1月4日，已生成16万行形式化的拓扑学代码。其中大部分工作（约13万行）是在短短两周内完成的，即从12月22日至1月4日，所花费的大语言模型订阅成本约为100美元。这些成果包括：乌雷松引理（Urysohn's lemma）的3千行证明、乌雷松度量化定理（Urysohn's Metrization theorem）的2千行证明、蒂策扩展定理（Tietze extension theorem）超过1万行的证明，以及其他众多结果（总计超过1500个引理和定理）。该方法极为简单且成本低廉：构建一个大语言模型与具备核心基础库的、速度合理的证明检查器之间的长期反馈循环。目前，该大语言模型以ChatGPT（主要是5.2版本）或Claude Sonnet（4.5版本）实现，并通过相应的Codex或Claude Code命令行接口运行；证明检查器采用查德·布朗（Chad Brown）开发的高阶集合论系统Megalodon，核心库则基于布朗对基本集合论和超实数（包含实数等）的形式化工作。其余部分涉及一些提示工程与技术选择，我们将在下文详述。鉴于该项目进展迅速、成本极低、所用交互式定理证明系统/库几乎不为人知，且整体设置极为简单并可被任何人复现，我们相信，在2026年，无论使用何种证明助手，（自动）形式化工作都可能变得异常容易并广泛普及。

论文试图解决数学形式化（尤其是拓扑学）过程中效率低下、成本高昂且依赖专家人力的问题。通过自动化方法将经典数学教材（如Munkres的《拓扑学》）中的定理和证明自动转化为机器可验证的形式，是一个尚未被广泛解决的新问题，尤其在使用低成本、通用大模型与轻量级证明系统结合的路径上几乎未被探索。

提出一种简单而高效的反馈循环架构：将大型语言模型（LLM，如ChatGPT或Claude Sonnet）与快速的高阶集合论证明检查器Megalodon相结合，利用Brown已有的基础库（集合论与超实数形式化）作为核心基础设施，通过精心设计的提示工程实现持续自动形式化。关键创新在于不依赖复杂的强化学习或专用训练模型，而是通过廉价、现成的工具链实现大规模自动形式化，显著降低门槛和成本。

项目在极短时间内（约两周）生成了13万行形式化代码，总规模达16万行，包含1500多个定理的证明，如Urysohn引理（3k行）、Urysohn度量化定理（2k行）和Tietze扩张定理（超10k行）。整个过程仅花费约100美元LLM订阅费用，展示了惊人的性价比。技术栈完全基于公开可用工具（Codex/Claude CLI + Megalodon），未使用专有模型或复杂训练流程。实验设计体现为长期运行的交互式形式化流水线，虽未明确提及开源代码，但所用系统均为可访问工具，具备高度可复现性。未来值得深入研究的方向包括该方法向其他数学领域（如代数拓扑、微分几何）的迁移能力，以及如何进一步提升证明合成的准确率与自动化程度。

1. Autoformalization with Large Language Models 2. Formalizing Mathematics: Challenges and Opportunities 3. Lean Copilot: Action-Based Learning for Interactive Theorem Proving 4. Proof Artifact Generation Using Neural Language Models 5. Natural Proof Generation for Formal Mathematical Statements