仅需$100订阅费生成13万行代码：大模型实现数学自动形式化突破

Josef Urban团队发布最新研究成果，展示了如何利用现有的ChatGPT和Claude模型，在短短两周内自动生成了超过13万行的形式化拓扑学代码。该方法通过建立大语言模型与证明检查器之间的持续反馈闭环，以约100美元的低廉成本完成了包括乌雷松引理和度量化定理在内的复杂证明。这一成果表明，结合简单的提示词工程与基础数学库，AI已能让高难度的数学形式化工作变得简单、廉价且易于普及。