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

arXiv: https://arxiv.org/abs/2610.04829 · HTML: https://mlsanity.com/paper/2610.04829/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Software engineering coding agents, one of 16 directions in LLM agents and tool use.
- Builds on 9 of its 9 references that are in the map.
- First posted on arXiv 4 Oct 2026.

## Placed in

- LLM agents and tool use / [Software engineering coding agents](https://mlsanity.com/agents/software-engineering-coding-agents/)

## Builds on (most cited first, 9 of 9)

- [Reflexion: Language Agents with Verbal Reinforcement Learning](https://mlsanity.com/paper/2303.11366/) (2023)
- [Large Language Models Cannot Self-Correct Reasoning Yet](https://mlsanity.com/paper/2310.01798/) (2023)
- [Why Do Multi-Agent LLM Systems Fail?](https://mlsanity.com/paper/2503.13657/) (2025)
- [AgentPoison: Red-teaming LLM Agents via Poisoning Memory or Knowledge Bases](https://mlsanity.com/paper/2407.12784/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://mlsanity.com/paper/2502.03438/) (2025)
- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [Interactive Error Correcting Codes Over Binary Erasure Channels Resilient to >frac12 Adversarial Corruption](https://mlsanity.com/paper/2111.04181/) (2021)

## Abstract (arXiv)

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. We instrumented such a system end to end and analyzed 51,754 traced observations across three full runs (186 hours, 5,694). We find three connected failure modes. First, the three-model verifier requires unanimity and treats parse or API failure as non-approval; in 10 of 12 verification events, one member returned no parseable output or an API error, making acceptance arithmetically impossible without surfacing an error. Second, when the ensemble did function, one verifier approved 3 attempts that GPT rejected, each claiming to resolve the open problem; a single-verifier design would therefore have announced a solution three times. Third, because nothing could be approved, every review was a refutation, yet the lemma extractor mines reviews as well as proofs: 24 of 93 lemmas (26%) were extracted from rejected arguments with their refutational context removed. Taken together, these findings show that without external verification, supervision is itself a critical trust boundary: systems must distinguish abstention from rejection, preserve useful disagreement, and preserve the provenance and polarity of information before it becomes future context.