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.
[Read More]🎤 Invited Talk at SCML-2026
Formalization and Automated Reasoning in the Age of LLMs, Hagenberg, Austria
Prof. Cezary Kaliszyk gave an invited talk at SCML-2026, the conference on Symbolic Computation and Machine Learning, held July 6–8, 2026 in Hagenberg, Austria.
His talk, “Formalization and Automated Reasoning in the Age of LLMs”, was presented on Monday, July 6, and discussed how large language models are reshaping formalization and automated reasoning. The slides are available here.