# QED: An Open-Source Multi-Agent System for Generating Mathematical Proofs on Open Problems

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

## Key facts

- Cited by 13 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 47 references that are in the map.
- First posted on arXiv 27 Apr 2026.

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

- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Self-Consistency Improves Chain of Thought Reasoning in Language Models](https://mlsanity.com/paper/2203.11171/) (2022)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI](https://mlsanity.com/paper/2411.04872/) (2024)
- [Reward Hacking in the Era of Large Models: Mechanisms, Emergent Misalignment, Challenges](https://mlsanity.com/paper/2604.13602/) (2026)
- [Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving](https://mlsanity.com/paper/2404.07382/) (2024)
- [ALMAS: an Autonomous LLM-based Multi-Agent Software Engineering Framework](https://mlsanity.com/paper/2510.03463/) (2025)
- [Next-Token Prediction Task Assumes Optimal Data Ordering for LLM Training in Proof Generation](https://mlsanity.com/paper/2411.00863/) (2024)

## Built on by (most cited first, 13 of 13)

- [Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory](https://mlsanity.com/paper/2607.06447/) (2026)
- [MechMath Agent Team: LLM Driven Agents for Mathematical Research](https://mlsanity.com/paper/2607.04394/) (2026)
- [Albilich: Steerable Proof-State Orchestration for LLM-Based Mathematical Research with CAS Integration](https://mlsanity.com/paper/2607.27705/) (2026)
- [VALG: An Agentic System for ML Theory Research](https://mlsanity.com/paper/2608.13060/) (2026)
- [The Problem Is the Problem: Towards Scalable Mathematical Discovery](https://mlsanity.com/paper/2608.16977/) (2026)
- [ReasFlow: Assisting Reasoning-Centric Scientific Discovery in Applied Mathematics via a Knowledge-Based Multi-Agent System](https://mlsanity.com/paper/2607.14178/) (2026)
- [MECA: A Mechanism-Centered Agent for Constructing Well-Specified and Valuable Mathematical Conjectures](https://mlsanity.com/paper/2607.27709/) (2026)
- [Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science](https://mlsanity.com/paper/2609.15983/) (2026)
- [Lower Bounds for Advection-Diffusion Equations: An Exploration with AI-Generated Proofs](https://mlsanity.com/paper/2605.20623/) (2026)
- [Andy: A Mathematical Agent for Rigorous Proof and Autonomous Research](https://mlsanity.com/paper/2608.15052/) (2026)
- [EULER: Exploring Underused Links with Evidence-Checked Return for Multi-Agent Mathematical Discovery](https://mlsanity.com/paper/2609.00032/) (2026)
- [TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science](https://mlsanity.com/paper/2609.35606/) (2026)
- [Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization](https://mlsanity.com/paper/2609.39228/) (2026)

## Abstract (arXiv)

We present QED, an open-source multi-agent system that turns human-provided research questions into complete mathematical proofs without further human guidance. Its pipeline is designed to overcome common failures of single-query proof generation by separating planning, proving, and verification: a decomposition agent structures the proof search, prover agents generate candidate arguments, and verifier agents check correctness. In collaboration with domain experts, we evaluated QED on 18 research-level projects of varying difficulty. QED produced five original works across algebraic geometry, fluid PDEs, probability, and inverse problems. Expert assessments regard these works as solid specialized research contributions, with three comparable in difficulty and scope to work commonly published in established specialist mathematics venues. QED is released at https://github.com/proofQED/QED.