Our paper Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents, by Chad E. Brown, Cezary Kaliszyk, and Josef Urban, has been published in the proceedings of the Workshop on Practical Aspects of Automated Reasoning (PAAR 2026), held as part of FLoC 2026 in Lisbon, Portugal. The paper explores large-scale autoformalization of algebraic topology using a simulated bounty marketplace, where multiple LLM agents propose formal lemmas, attach bounties, and compete to discharge proof obligations, scaling collaborative formalization in a decentralized fashion.
The paper is available from our Publications page, together with a link to the arXiv preprint.