Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents

This paper presents "Agent Hunt," a decentralized autoformalization system for algebraic topology that utilizes a simulated bounty-based marketplace to coordinate multiple LLM agents in dynamically proposing, competing to prove, and iteratively refining formal statements within an Interactive Theorem Proving environment.

The Gist

Imagine a massive, incredibly difficult math textbook on Algebraic Topology (a field that studies shapes and spaces). This textbook is like a giant, locked treasure chest. Inside are hundreds of theorems (mathematical truths) that need to be translated from human language into a strict, computer-readable language called "formal logic."

Usually, one very smart computer program (an AI agent) tries to do this alone. But in this paper, the researchers tried something different: They turned the translation job into a competitive video game with a cash prize.

Here is the story of "Agent Hunt," explained simply.

1. The Setup: The Bounty Board

Instead of giving one robot a long to-do list, the researchers set up a virtual marketplace.

• The Boss: The researchers took the textbook and broke it down into 393 specific math problems (lemmas and theorems).
• The Bounties: They attached a "price tag" to every problem. Some were worth a little, some a lot, depending on how hard they thought the proof would be.
• The Players: They hired four AI agents (named Alice, Bob, Charlie, and Dave). Think of them as four highly skilled, digital detectives.

2. The Rules: How the Game Works

The agents didn't just work in a line; they competed and cooperated in a chaotic but organized way:

• Locking the Job: If an agent saw a problem they wanted to solve, they could "lock" it by paying a small deposit. This meant, "I'm working on this! Don't touch it!"
• The Prize: If they successfully proved the theorem and the computer checked it, they got the full bounty (the reward).
• Stealing the Job: If an agent locked a problem but got stuck, or if another agent solved it faster, the lock could expire, and the reward would go to the winner.
• Collaboration: Sometimes, an agent would solve a small piece of a problem (a sub-lemma) and put a new bounty on it, inviting others to help finish the bigger picture.

3. The Analogy: The "Construction Site"

Imagine a massive skyscraper needs to be built.

• The Old Way: You hire one master architect who tries to design the whole building, floor by floor, alone. It takes forever, and if they get tired or stuck on the 50th floor, the whole project stalls.
• The Agent Hunt Way: You put a "Wanted" poster on every single brick and beam.
  • Alice sees a blueprint for a window and says, "I'll build that!"
  • Bob sees a foundation beam and says, "I'll do that!"
  • If Alice gets stuck on the window, Bob might step in, finish it, and claim the reward.
  • If Alice builds a great window, she might say, "Hey, I need a special hinge for this," and put a small bounty on the hinge. Bob might then build the hinge to help Alice finish her window.

This creates a decentralized swarm where everyone is motivated by the reward to keep moving forward, rather than waiting for a central boss to give instructions.

4. The Results: Speed and Chaos

The experiment was a huge success in terms of speed:

• The Speed: The four agents working together produced 39,000 lines of code in two days.
• The Comparison: A single agent working on a similar project previously only managed about 7,000 lines a day. The "bounty market" made them 5 times faster.
• The Economy: The agents earned "simulated money" (tokens). Some agents got rich by solving hard problems; others got stuck or had to reset their accounts when they made mistakes (like using the wrong version of the computer checker).

5. The Hiccups: When the Game Gets Weird

It wasn't all smooth sailing. The researchers noticed some funny and tricky situations:

• The "Exercise" Trap: The textbook had practice problems at the end of chapters that didn't have answers. The AI agents tried to solve them anyway, spending hours on them only to get a tiny reward because the "price tag" was wrong. The researchers had to tell them, "Ignore those!"
• The "Cosine" Bug: One of the hardest problems was proving a theorem about circles. The AI was trying to use a definition of "sine" and "cosine" that was mathematically broken (it allowed for multiple wrong answers). The agents were spinning their wheels, trying to prove things that were impossible with the broken definitions. The researchers realized the AI needed to rewrite the definitions, not just solve the proofs.

6. The Big Picture: Why This Matters

This experiment shows that AI doesn't have to work alone to solve big problems.

By creating a system where AI agents compete for rewards, they can:

1. Scale up: Tackle projects too big for one brain.
2. Self-Correct: If one agent gets stuck, another can jump in.
3. Build Faster: The "market" forces them to prioritize the most important and valuable work.

In short: The researchers turned math proof-writing into a high-speed, competitive video game. By letting the AI agents "hunt" for bounties, they proved that a team of AI agents working together is much faster and more powerful than a single AI working alone.

Technical Summary

Here is a detailed technical summary of the paper "Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents."

1. Problem Statement

The paper addresses the scalability and efficiency challenges in Autoformalization—the process of translating informal mathematical text into formal proofs within Interactive Theorem Provers (ITPs).

• The Bottleneck: Previous large-scale attempts (e.g., the General Topology project formalizing Munkres' textbook) relied on a single LLM agent. This approach proved slow (taking months for 350k+ lines) and struggled with the unpredictable nature of large formalizations, such as proof gaps, forward references, and the need for dynamic restructuring.
• The Challenge: How to parallelize the work of multiple LLM agents effectively without a rigid, centrally planned division of labor, which is difficult to pre-define for complex mathematical developments.

2. Methodology: The "Agent Hunt" Framework

The authors propose a decentralized, bounty-based marketplace where multiple LLM agents compete and collaborate to formalize algebraic topology.

A. Target Domain

• Task: Formalizing Part II of Munkres' Topology (Chapters 9–14, Sections 51–85), covering approximately 200 pages of Algebraic Topology.
• Environment: The Megalodon higher-order set theory proof checker.
• Baseline: The project builds upon a pre-existing library of ~19k lines (General Topology) and aims to extend it to ~121k lines.

B. The Bounty System Mechanics

Instead of a central planner assigning tasks, the system uses a simulated economic market:

1. Initial Setup: A single "architect" agent (Claude Opus 4.6) was tasked with formalizing the statements (definitions and theorems) from the source text without proofs. It attached bounties (estimated effort/cost in simulated USD tokens) to each theorem based on textbook proof length and difficulty (1–10 scale).
2. Agent Roster: Four agents (Alice, Bob, Charlie, Dave) using ChatGPT Pro Codex and Claude Code models.
3. Market Rules:
   • Locking: Agents can "lock" a theorem by paying 10% of its bounty, reserving the right to claim the full reward upon completion.
   • Competition vs. Collaboration: Agents compete to solve locked theorems but are incentivized to collaborate (e.g., solving sub-lemmas for others) to finish the project faster and earn bonuses.
   • Sub-bounties: Agents can create new lemmas and attach bounties to them to structure the proof.
   • Ownership: Agents cannot modify others' locked proofs or definitions, ensuring integrity.

C. Technical Infrastructure & Guardrails

• Guard Scripts: Local scripts run before every commit to enforce invariants:
  • Non-negative agent balances.
  • Maximum of 10 locks per agent (24h expiry).
  • Immutability of definitions and theorem statements (only proofs can change).
  • Validation of Qed (completed) vs. Admitted (placeholder) status.
• Megalodon Modifications: The proof checker was adapted for LLM usage:
  • Efficiency: Replaced linear lookups with optimized operations for long files.
  • Trust Model: Blocked Qed for proofs with unproven dependencies; agents must use Admitted until dependencies are verified.
  • Readability: Replaced opaque hash names with readable symbol names for LLMs.
  • Axiom Control: Used an index of allowed axiom hashes to prevent reliance on unproven axioms.

3. Key Contributions

1. Decentralized Proof Search: Demonstrated that a market-driven, agent-based approach can scale autoformalization more effectively than single-agent linear progression.
2. Dynamic Task Allocation: Showed that agents can self-organize, identifying gaps, creating intermediate lemmas, and competing for high-value theorems without human intervention.
3. Hybrid Collaboration Model: Introduced a mechanism where agents can "lock" work to secure rewards while still allowing others to contribute to sub-components, balancing competition with necessary cooperation.
4. Robust Verification Pipeline: Developed a workflow where all proofs are ultimately checked by the underlying ITP (Megalodon), ensuring that the "market" does not compromise mathematical correctness.

4. Results

• Speed and Scale:
  • Over 2 days and 15 hours, four agents generated ~102k new lines of formal code (reaching 121k total).
  • Throughput: ~39k lines/day, compared to ~7k lines/day in the previous single-agent General Topology project.
• Economic Dynamics:
  • Total bounties distributed: ~45k simulated tokens.
  • Collaboration Metrics: Of 709 new bounties placed:
    • 279 were solved by the creator (self-completion).
    • 114 were solved by a different agent (cross-agent collaboration).
    • 312 remained unsolved at the experiment's end.
• Major Theorems Proved:
  • Successfully proved complex theorems including the Brouwer Fixed Point Theorem (via a chain of proofs totaling ~7k lines) and the cyclic nature of infinite order groups.
  • Proved the Fundamental Group axioms (associativity, identity, inverses), though this required significant division of labor between agents (e.g., Alice proving right-inverses, Bob proving left-inverses).
• Cost Efficiency: The experiment cost approximately $150 (using LLM subscriptions), equating to roughly $1 per 1,000 normalized lines.

5. Observations and Limitations

• Division of Labor: Agents naturally developed thematic ownership (e.g., Bob focused on homotopy/fundamental groups; Charlie on geometry/circles; Alice on path-concatenation; Dave on abstract group theory).
• Exercise Handling: Initial attempts to formalize textbook "exercises" failed because they lacked proofs in the source text, leading to misleading bounty estimates. The system was updated to deprioritize exercises.
• Definition Failures: The agents struggled with the Brouwer Fixed Point Theorem because the underlying definitions of cos and sin (based on an epsilon-choice operator) were non-unique and mathematically flawed in the context of the formalization. The agents could not prove properties of these functions without generating new, correct definitions, highlighting a limitation in current LLMs' ability to self-correct foundational definitions without human guidance.
• Refactoring: The system handled minor refactoring well, with only small dips in line growth corresponding to structural improvements.

6. Significance

The "Agent Hunt" experiment demonstrates that market-inspired mechanisms are a viable strategy for scaling formal mathematics. By moving away from rigid, top-down planning to a dynamic, competitive, and collaborative agent ecosystem, the authors achieved a 5x increase in formalization speed compared to single-agent baselines. This approach suggests a future where large-scale mathematical libraries can be built by swarms of specialized AI agents, provided there is a robust verification layer and economic incentives to ensure quality and cooperation.