Viva La Vida: Verification and Accumulation Failures in Multi-Agent Proof Search

Benji Xu, Ken Zheng, Noah Han

When an agentic prover works on an open problem, there is no proof assistant to fall back on: its verifier and lemma library are ultimately language models judging model outputs. W…