130k Lines of Formal Topology: Simple and Cheap Autoformalization for Everyone?
6 hours ago
- #LLM
- #General Topology
- #Autoformalization
- A project has autoformalized a large portion of general topology from the Munkres textbook.
- The project produced 160k lines of formalized topology, with 130k lines completed in two weeks.
- Key achievements include proofs of Urysohn's lemma (3k lines), Urysohn's Metrization theorem (2k lines), and the Tietze extension theorem (10k lines).
- The approach involves a feedback loop between an LLM (ChatGPT 5.2 or Claude Sonnet 4.5) and a proof checker (Megalodon).
- The total cost for the LLM subscription was about $100.
- The project suggests that autoformalization may become easy and ubiquitous in 2026.