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

TL;DR

QED is an open-source multi-agent system designed to address key failure modes in AI-generated mathematical proofs, successfully producing original proofs for open problems in analysis and PDEs.

Contribution

The paper introduces QED, a multi-agent proof system that systematically tackles failure modes in AI proof generation, achieving verified original proofs for research-level problems.

Findings

QED produced correct proofs for three out of five open problems.

The system addresses seven identified failure modes in proof generation.

QED's architecture led to verified, nontrivial proofs by domain experts.

Abstract

We explore a central question in AI for mathematics: can AI systems produce original, nontrivial proofs for open research problems? Despite strong benchmark performance, producing genuinely novel proofs remains an outstanding challenge for LLMs. Through systematic experiments with frontier LLMs on research-level proof tasks, we identify seven failure modes that prevent reliable proof generation, including context contamination, citation hallucination, hand-waving on key steps and misallocation of proof effort, unstable proof plans, unfocused verification, problem modification and single-model bottleneck. We argue that the gap between benchmark success and research-level proving is primarily one of system design, due to those failure modes. We present QED, an open-source multi-agent proof system in which each architectural decision directly addresses a specific failure mode. Evaluated on five open problems in applied analysis and PDEs contributed by domain experts, QED produces correct proofs for three problems, each verified by the contributing experts as original and nontrivial. QED is released as open-source software at https://github.com/proofQED/QED.