Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents

Chad E. Brown, Cezary Kaliszyk, Josef Urban

We describe an experiment in large-scale autoformalization of algebraic topology in an Interactive Theorem Proving (ITP) environment, where the workload is distributed among multip…