This is a brief description of a project that has already autoformalized a large portion of the general topology from the Munkres textbook (which has in total 241 pages in 7 chapters and 39 sections). The project has been running since November 21, 2025 and has as of January 4, 2026, produced 160k lines of formalized topology. Most of it (about 130k lines) have been done in two weeks,from December 22 to January 4, for an LLM subscription cost of about \$100. This includes a 3k-line proof of Urysohn's lemma, a 2k-line proof of Urysohn's Metrization theorem, over 10k-line proof of the Tietze extension theorem, and many more (in total over 1.5k lemmas/theorems). The approach is quite simple and cheap: build a long-running feedback loop between an LLM and a reasonably fast proof checker equipped with a core foundational library. The LLM is now instantiated as ChatGPT (mostly 5.2) or Claude Sonnet (4.5) run through the respective Codex or Claude Code command line interfaces. The proof checker is Chad Brown's higher-order set theory system Megalodon, and the core library is Brown's formalization of basic set theory and surreal numbers (including reals, etc). The rest is some prompt engineering and technical choices which we describe here. Based on the fast progress, low cost, virtually unknown ITP/library, and the simple setup available to everyone, we believe that (auto)formalization may become quite easy and ubiquitous in 2026, regardless of which proof assistant is used.

翻译：本文简要介绍了一个已自动形式化Munkres教材中大部分一般拓扑内容的项目（该教材共7章39节241页）。该项目自2025年11月21日启动，截至2026年1月4日已生成16万行形式化拓扑代码。其中主要部分（约13万行）在两周内（12月22日至1月4日）完成，仅消耗约100美元的大语言模型订阅费用。成果包括：3000行的乌雷松引理证明、2000行的乌雷松度量化定理证明、超过1万行的蒂茨扩张定理证明，以及总计超过1500个引理/定理的形式化。该方法极为简易且成本低廉：在大语言模型与配备核心基础库的快速证明检查器之间建立长期运行的反馈循环。当前大语言模型实例为通过相应Codex或Claude Code命令行接口运行的ChatGPT（主要为5.2版本）或Claude Sonnet（4.5版本）。证明检查器采用Chad Brown的高阶集合论系统Megalodon，核心库为Brown开发的基础集合论与超现实数（含实数等）形式化库。其余部分涉及本文所述的提示工程与技术方案选择。基于其快速进展、低廉成本、几乎未被知晓的交互式定理证明器/库资源以及人人可用的简易配置，我们相信（自动）形式化技术可能在2026年变得异常简单且无处不在，无论采用何种证明辅助工具皆可适用。