Source-linked AI summary
130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?
Josef Urban
TL;DR
This ongoing experiment examines whether LLM-based coding agents can support accessible, low-cost formalization with a proof assistant and foundational library. It uses feedback from proof checking to develop topology formalizations, while encountering external dependencies and subscription usage limits.
Problem
The project investigates whether recent progress with coding agents can support broader participation in formalization, amid concerns that potential contributors have been diverted toward AI or AR.
Method
The experiment combines LLM-based command-line coding agents with the Megalodon higher-order set-theory proof checker and Brown’s foundational library.
Results
The experiment produced formalized topology including correct formalizations of connectedness, closed subspaces of compact spaces, and related textbook results.
Takeaways & Limitations
The authors conclude that AI-assisted formalization may become broadly accessible and that its future remains open across proof assistants.
Takeaways & Limitations
The approach is constrained by external dependencies such as infinite-sum and uniform-convergence results, and by subscription usage limits.
Abstract
from arXiv · showhide
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.
1 Introduction
The project explores an ongoing, feedback-driven experiment in autoformalizing topology with coding agents and the Megalodon proof checker. Its setup combines a foundational library, repeated prompts, sandboxing, and workflow rules intended to sustain broad, reliable progress.
- Scope: The write-up presents the work as an ongoing experiment whose assessment may change as it proceeds.The stated purpose is largely to let others try the approach in their own settings.
- Project setup: The experiment uses LLM coding agents with Megalodon to formalize topology on top of Brown’s foundational set-theory and surreal-number library.The setup also uses sandboxing and additional prompting tools.
- Motivation: The project was motivated by reports that coding agents could complete substantial formal proofs, including a 13k-line Lean formalization of Ramsey(3,6).Those reports prompted the move to topology with Megalodon and command-line agents.
- Scale: About 130k lines were produced by the latest setup, which had been nearly stable since December 22.The setup used a ChatGPT Pro subscription and the Megalodon proof checker with Brown’s core library.
- Workflow: The workflow repeatedly prompts the coding agent, restricts edits to the topology section, and uses instructions to preserve work, remove admits, and prioritize major theorems.The prompt was reportedly issued about 1000–2000 times during two weeks.
4 Other Prompts
The prompting strategy evolved from exploratory instructions toward long-running, autonomous work and targeted interventions on difficult proofs. Focused prompts completed major theorem efforts but could also encourage undesirable shortcuts without the general rules.
- 4.1 Initial: Initial prompts asked the agent to read the topology source, formalize it in Megalodon, verify compilation, and make numbered backups.The early sequence alternated between proof attempts and broader coverage of definitions and top-level theorems.
- 4.1 Initial: The early instructions shifted emphasis from detailed proofs toward covering textbook definitions and top-level theorems and lemmas.This was intended to push the formalization forward more broadly.
- 4.1 Initial: Independent runs eventually lasted over 1 hour and sometimes 2 hours before another prompt was supplied.The same prompt was often repeated until prompting was automated.
- 4.2 Focused Prompting: A December 31 focused prompt made finishing Urysohn’s lemma the agent’s singular goal.The intervention followed the agent’s partial work on the theorem and its tendency to switch tasks.
- 4.2 Focused Prompting: The focused Urysohn effort finished a 3k-line proof by the end of 2025, although the system initially tried forbidden shortcuts.The general CLAUDE.md rules were re-emphasized afterward.
- 4.2 Focused Prompting: A later focused prompt targeted Tietze_stepII_real_extension_nonempty and required completion before switching tasks.The prompt also instructed the agent to follow CLAUDE.md exactly.
- 4.2 Focused Prompting: The Tietze intervention finished a 10k-line proof and its prerequisites after about 20 hours.The author presents this as a way to combine automated broad progress with occasional user reprioritization.
5 Further Utilities
The project added utilities for theorem-dependency visibility and explored automated theorem proving, while encountering limitations in proof search and workflow control. Formalization growth accelerated after switching to ChatGPT Pro.
- Hammer attempts: The higher-order hammer aby can export Megalodon problems to TH0 TPTP and call higher-order Vampire, but it has not yet been very useful.The setup lacks proof reconstruction and may need caching, premise selection, and smarter ATP reruns.
- Dependency guidance: A theorem-status utility reports each theorem’s proof status, partial-proof length, and dependencies to help the LLM identify bottlenecks.The author says this appears to have improved the LLM’s orientation.
- Workflow problems: The workflow faced recurring problems with incomplete specifications, preference for easy lemmas, and difficulty maintaining awareness across sections.The author describes the trade-off between deep theorem proving and broad project awareness as nontrivial.
- Formalization growth: Table 1 relates commit number to the number of formalization lines and shows accelerated growth after switching to ChatGPT Pro.The table is described as reporting lines after each 100 backups, corresponding to commits.
8 Resources Used
The project used paid LLM subscriptions and hourly cost tracking to support automated formalization. Early $20/month subscriptions produced 30k lines in about a month, while later usage exceeded the Pro subscription’s weekly credits.
- Hourly cost reports tracked 72 hours of LLM usage, including a restart related to compactification.Table 2 presents the reports in six columns of twelve hours.
- 30k lines were produced in about a month using $20/month Codex or Claude Code subscriptions.The author describes this output as potentially useful despite quickly depleting usage credits.
- The $200/month Pro subscription reached its weekly usage limit in both weeks of use.In the second week, credits were depleted three days before reset, about eight hours after the Tietze proof was completed.
9 Miscellaneous Comments
The experiment encountered limitations from finite context windows, hard session-size limits, growing proof-checking time, and the lack of a full analysis of successes and failures. The author used session-file resets and retained the unsplit proof file because LLM usage remained the main bottleneck.
- The author has not yet had time and energy to conduct a full-scale analysis of what worked and failed.Complete logs and public git commits could support future automated analysis and prompt improvement.
- 9.1 Context Compactification: Compactification can behave unpredictably because coding agents discard nonessential context from limited windows.The author identifies this as a major issue with the technology.
- 9.1 Context Compactification: Two hard session limits were reached when ChatGPT session files grew to about 252MB and 351MB.The author reset each session to an earlier 65MB version rather than starting completely over, calling the workaround unsupported and dangerous.
- 9.2 Running Megalodon: Megalodon verification grew from under 1s initially to 32s when the file reached almost 170k lines and 8MB.The author has not split the file or admitted finished theorems because proofs may still be refactored and LLM usage remains the larger bottleneck.
10 Major Theorems Proved
The project reports a broad set of formally proved topology results, including major compactness, separation, metrization, connectedness, and continuity theorems. Table 3 organizes selected proved results by direct Megalodon proof length and dependency count, while Table 4 records an assessment of 30 major results.
- Table 3: Table 3 lists proved topology theorems exceeding 300 direct Megalodon proof lines, sorted by proof length and accompanied by dependency counts.The table may omit major results presented as easier corollaries, but the authors describe it as informative.
- Separation and metrization: 674 lines formalize metrizable spaces as normal, while 625 lines encode an embedding theorem via functions.Other long proofs include 600 lines for regular spaces with countable bases implying normality and 581 lines for second countability of Euclidean spaces.
- Compactness: 615 lines formalize that a compact space net has an accumulation point, while 590 lines cover the corresponding restricted result.The listed results also include finite-product compactness, compact-to-Hausdorff homeomorphism, and Heine–Borel closed-boundedness.
- Assessment: Table 4 presents ChatGPT’s selection and assessment of 30 major topology results, with exact theorem statements supplied in the Appendix.The assessment includes connectedness, compactness, product, subspace, and continuity results whose formalizations are described as faithful, reusable, or robust.
11 The Battle of the Tietze Hill
The Tietze extension formalization became the project’s largest proof effort because the textbook argument depends on infinite sums, uniform convergence, and completeness infrastructure introduced later in the text. After substantial reorganization and wasted work, the project completed the nonempty-case Step II proof and the real-valued extension theorem.
- Completed proof: The completed Tietze Step II proof has no admits and contains 10,369 lines with 142 direct dependencies: 36 definitions and 106 theorems.The final update closed the temporary admit in Htail_budget by adding the missing HgN0xS lemma and completing the final transitivity step.
- Dependency gap: The textbook Tietze proof depends on infinite sums of real functions and uniform convergence, an external dependency absent from the textbook.The agent initially responded by unrolling the infinite construction 12 times, producing about 6k lines that were not useful for the final proof.
- Dependency gap: 11 iterations expanded the proof from 865 to 5408 lines over nearly 4 hours because completeness tools appear only in Munkres section 43, after Tietze in section 35.The work required moving uniform-limit infrastructure earlier and adding temporary early stubs to avoid forward references.
- Formalized results: The formalized bounded-interval theorem extends a continuous map from a closed subspace of a normal space while preserving its interval bounds.The real-valued theorem separately guarantees a continuous extension agreeing with the original map on the closed subspace.
12 Conclusion
The project reports rapid, low-cost progress with an LLM–proof-checker workflow and suggests that autoformalizing substantial portions of mathematical texts may become widespread in 2026. It also acknowledges that the approach may eventually encounter limits.
- Conclusion: The project reports that a simple LLM–proof-checker workflow achieved rapid progress at low cost using Megalodon and coding agents.The authors present the outcome as surprising and exciting while emphasizing uncertainty about where the approach will lead.
- Conclusion: The authors speculate that most reasonably written mathematics textbooks and papers may be autoformalized in 2026, while acknowledging possible eventual limits.This is explicitly framed as a possibility rather than a definite prediction.
A Listing of the Major Theorems in LaTeX and Megalodon
The formalization covers major results in connectedness, compactness, continuity, separation, countability, metrization, extension, and paracompactness. The listed Megalodon statements closely mirror textbook theorems, including foundational lemmas and advanced results such as Urysohn's lemma and the Tietze extension theorem.
- Continuity and products: The pasting lemma formalizes continuity of a map from continuity on two closed pieces and their intersection.
- Continuity and products: A map into a product is continuous exactly when both component maps are continuous, and finite products preserve connectedness.
- Compactness: Compactness results include inheritance by closed subspaces, closedness of compact subspaces in Hausdorff spaces, compact-to-Hausdorff bijections, finite-product compactness, the tube lemma, and Heine–Borel.
- Separation and countability: Countable bases yield countable subcovers and countable dense subsets, while regular spaces with countable bases are normal and every such compact Hausdorff space is normal.
- Major advanced theorems: The listing includes Urysohn's lemma, the Urysohn metrization theorem, the Tietze extension theorem, paracompactness results, and continuity of the evaluation map.
- Connectedness: Connectedness results include separation-based nonconnectedness, connected unions with a common point, continuous images, components, and connectedness between a subspace and its closure.