QED: An Open-Source Multi-Agent System for Generating Mathematical Proofs on Open Problems
Not on the map. Why?
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.
Key facts. Cited by 9 papers in the map (data through 7 Oct 2026). Builds on 9 of its 47 references that are in the map. First posted on arXiv 27 Apr 2026.
Builds on
9 of 47 references.
References · 9
- 2022Chain-of-Thought Prompting Elicits Reasoning in Large Language Modelscited by 12,302
- 2021Training Verifiers to Solve Math Word Problemscited by 9,743
- 2022Self-Consistency Improves Chain of Thought Reasoning in Language Modelscited by 5,601
- 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,203
- 2024FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AIcited by 227
- 2026Reward Hacking in the Era of Large Models: Mechanisms, Emergent Misalignment, Challengescited by 30
- 2024Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Provingcited by 11
- 2025ALMAS: an Autonomous LLM-based Multi-Agent Software Engineering Frameworkcited by 4
- 2024Next-Token Prediction Task Assumes Optimal Data Ordering for LLM Training in Proof Generationcited by 2
Built on by
Citing papers per year: 2026: 9.
9 papers.
- 2026Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memorycited by 5
- 2026MechMath Agent Team: LLM Driven Agents for Mathematical Researchcited by 3
- 2026ReasFlow: Assisting Reasoning-Centric Scientific Discovery in Applied Mathematics via a Knowledge-Based Multi-Agent Systemcited by 1
- 2026Albilich: Steerable Proof-State Orchestration for LLM-Based Mathematical Research with CAS Integrationcited by 1
- 2026VALG: An Agentic System for ML Theory Researchcited by 1
- 2026Andy: A Mathematical Agent for Rigorous Proof and Autonomous Researchcited by 0
- 2026Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Sciencecited by 0
- 2026TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Sciencecited by 0
- 2026Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalizationcited by 0
- 2026Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization30 Sep 2026
- 2026TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science28 Sep 2026
- 2026Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science14 Sep 2026
- 2026Andy: A Mathematical Agent for Rigorous Proof and Autonomous Research15 Aug 2026
- 2026VALG: An Agentic System for ML Theory Research13 Aug 2026
- 2026Albilich: Steerable Proof-State Orchestration for LLM-Based Mathematical Research with CAS Integration30 Jul 2026
- 2026ReasFlow: Assisting Reasoning-Centric Scientific Discovery in Applied Mathematics via a Knowledge-Based Multi-Agent System15 Jul 2026
- 2026Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory7 Jul 2026
- 2026MechMath Agent Team: LLM Driven Agents for Mathematical Research5 Jul 2026