用奖金机制让AI代理协作证明拓扑学定理，自动构建新理论。
Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents
- AI代理在系统中竞标新定理，自动生成证明并争夺奖励。
- 通过动态竞争与协作，成功形式化多个代数拓扑定理。
- 适合对AI辅助数学证明、去中心化推理感兴趣的读者。
我们描述了一项大规模自动形式化代数拓扑的工作，采用基于LLM的编码代理在交互式定理证明（ITP）环境中协作完成任务。不同于静态集中规划，该系统模拟了基于奖金的市场机制：代理可动态提出新引理（形式化命题），为其设定奖金，并竞争完成证明以领取奖励。代理直接与交互式证明系统交互，可调用策略、检查证明状态与目标、分析策略成败，并迭代优化证明脚本。除构造证明外，代理还可引入新形式化定义和中间引理以组织开发。所有被接受的证明最终由底层证明助手验证。该设置探索了去中心化、协作式的证明搜索与理论构建，以及市场机制在扩展ITP自动形式化中的应用。
原文摘要 · Abstract (English)
We describe an experiment in large-scale autoformalization of algebraic topology in an Interactive Theorem Proving (ITP) environment, where the workload is distributed among multiple LLM-based coding agents. Rather than relying on static central planning, we implement a simulated bounty-based marketplace in which agents dynamically propose new lemmas (formal statements), attach bounties to them, and compete to discharge these proof obligations and claim the bounties. The agents interact directly with the interactive proof system: they can invoke tactics, inspect proof states and goals, analyze tactic successes and failures, and iteratively refine their proof scripts. In addition to constructing proofs, agents may introduce new formal definitions and intermediate lemmas to structure the development. All accepted proofs are ultimately checked and verified by the underlying proof assistant. This setting explores collaborative, decentralized proof search and theory building, and the use of market-inspired mechanisms to scale autoformalization in ITP.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。