AI RESEARCH
Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents
arXiv CS.AI
•
ArXi:2603.06737v1 Announce Type: cross 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.