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.

翻译：我们描述了一项在交互式定理证明环境中，对代数拓扑进行大规模自动形式化验证的实验，其中工作负载分布在多个基于LLM的编码智能体之间。我们采用模拟的悬赏型市场机制，而非依赖静态中央规划。在该机制中，智能体动态提出新引理（形式化陈述），为其附加悬赏，并相互竞争以完成这些证明义务并领取悬赏。这些智能体直接与交互式证明系统互动：它们可调用策略、检查证明状态与目标、分析策略的成功与失败，并迭代优化证明脚本。除构建证明外，智能体还可引入新的形式化定义和中间引理，以结构化开发过程。所有通过验证的证明最终都会由底层证明助手检查并确认。该实验探索了协作式、去中心化的证明搜索与理论构建过程，以及利用市场启发机制来扩展ITP中自动形式化验证的规模。