# Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents

arXiv: https://arxiv.org/abs/2603.06737 · HTML: https://mlsanity.com/paper/2603.06737/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use.
- Builds on 6 of its 9 references that are in the map.
- First posted on arXiv 6 Mar 2026.

## Placed in

- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)

## Builds on (most cited first, 6 of 6)

- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [Toolformer: Language Models Can Teach Themselves to Use Tools](https://mlsanity.com/paper/2302.04761/) (2023)
- [A formal proof of the Kepler conjecture](https://mlsanity.com/paper/1501.02155/) (2015)
- [130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?](https://mlsanity.com/paper/2601.03298/) (2026)
- [Hammering Higher Order Set Theory](https://mlsanity.com/paper/2509.08264/) (2025)
- [A Tale of Two Set Theories](https://mlsanity.com/paper/1907.08368/) (2019)

## Built on by (most cited first, 2 of 2)

- [Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance](https://mlsanity.com/paper/2606.14000/) (2026)
- [Choir: An Open Protocol for Distributed Multi-Agent Autoformalization](https://mlsanity.com/paper/2609.31903/) (2026)

## Abstract (arXiv)

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.