Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents

TL;DR

This paper presents a decentralized, market-inspired approach where multiple LLM-based agents collaboratively autoformalize algebraic topology proofs in an interactive theorem proving environment, demonstrating scalable proof development.

Contribution

It introduces a bounty-based marketplace mechanism for dynamic collaboration among LLM agents in autoformalization within an ITP setting, enabling scalable and decentralized proof search.

Findings

Agents successfully propose and discharge proof obligations

Market mechanism incentivizes effective collaboration

Proofs are verified by the proof assistant

Abstract

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.