130k Lines of Formal Topology: Simple and Cheap Autoformalization for Everyone?
2 months ago
- #LLM
- #General Topology
- #Autoformalization
- 一个项目已自动形式化了Munkres教材中大部分一般拓扑学内容
- 该项目生成了16万行形式化拓扑代码，其中13万行在两周内完成
- 主要成果包括乌雷松引理证明(3千行)、乌雷松度量化定理证明(2千行)和蒂茨扩张定理证明(1万行)
- 该方法采用大型语言模型(ChatGPT 5.2或Claude Sonnet 4.5)与证明检查器(Megalodon)之间的反馈循环
- 大型语言模型订阅总成本约100美元
- 该项目预示自动形式化技术可能在2026年变得简单且普及