# Munkres' General Topology Autoformalized in Isabelle/HOL

arXiv: https://arxiv.org/abs/2604.07455 · HTML: https://mlsanity.com/paper/2604.07455/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 23 references that are in the map.
- First posted on arXiv 8 Apr 2026.

## Builds on (most cited first, 6 of 6)

- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [First Experiments with Neural Translation of Informal to Formal Mathematics](https://mlsanity.com/paper/1805.06502/) (2018)
- [130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?](https://mlsanity.com/paper/2601.03298/) (2026)
- [Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Description](https://mlsanity.com/paper/1405.3451/) (2014)
- [Hammering Higher Order Set Theory](https://mlsanity.com/paper/2509.08264/) (2025)
- [Simple Type Theory is not too Simple: Grothendieck's Schemes without Dependent Types](https://mlsanity.com/paper/2104.09366/) (2021)

## Built on by (most cited first, 1 of 1)

- [Just Type It in Isabelle! AI Agents Drafting, Mechanizing, and Generalizing from Human Hints](https://mlsanity.com/paper/2604.15713/) (2026)

## Abstract (arXiv)

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--vCech 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.