130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone? (arxiv.org)

A groundbreaking project has successfully autoformalized a significant portion of general topology from the Munkres textbook, generating 160,000 lines of formalized content in just over a month, with around 130,000 lines produced in a focused two-week effort. This achievement, accomplished with a modest expense of about $100, includes complex proofs such as Urysohn's lemma and the Tietze extension theorem, among over 1,500 theorems and lemmas. The method involves a synergistic feedback loop between ChatGPT and Claude Sonnet as language models and Chad Brown's proof-checking system, Megalodon, supplemented by a foundational library focusing on set theory. This innovative approach could democratize formalization in mathematics and computer science by significantly lowering the cost and technical barrier to entry for researchers. With its simplicity and rapid development pace, the project suggests that autoformalization may soon become commonplace within the AI/ML community, potentially accelerating advancements in formal verification and logic applications across various disciplines. The implications for educational and research settings are profound, paving the way for wider adoption of formal methods and enhancing the reliability of mathematical proofs and algorithms.