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

Sign up for free to create and run prompts on this paper using GPT-5.

Overview

This paper asks a bold question: can AI not just solve practice math problems, but actually discover new, real math proofs that nobody knew before? The authors build a system called QED that works like a team of specialized AI “teammates” who plan, argue, fact-check, and double-check each other. They test QED on tough research problems (not textbook exercises), and in three cases it produces correct, original proofs that experts confirmed.

What questions did the paper ask?

The paper focuses on two simple-sounding but hard questions:

• Can today’s AI systems create new, correct proofs for open research problems (problems with no known solution yet)?
• If they struggle, what exactly goes wrong—and how can a better system design fix those problems?

How did they try to solve it?

They treat proof-writing like organizing a championship team, where each player has a role and there are referees who check everything carefully. Instead of asking one big AI model to do everything (which often fails), they built a multi-agent system with checks and balances.

Before building QED, the authors studied why big models fail at research-level proofs. They found seven common “failure modes.” Here they are in everyday language:

• Mixing roles: The same AI that writes the proof also “grades” it, so it’s biased toward accepting its own work.
• Making up sources: The AI cites theorems or papers that don’t actually exist or misquotes them.
• Skipping the hard parts: It hand-waves the toughest steps and over-explains the easy ones.
• Switching plans too much: It abandons a plan at the first difficulty and keeps jumping around.
• Unfocused checking: One checker tries to catch every kind of mistake at once and misses important errors.
• Quietly changing the question: It proves a slightly different (easier) problem and pretends it solved the original.
• One-model blind spots: Relying on a single model means inheriting its weaknesses with no backup.

To fix these, QED uses a structured approach. Think of it like a well-run lab class:

• Different roles, separate spaces: “Prover” AIs write proofs; separate “Verifier” AIs check them. The verifiers only see the problem and the proof, not the prover’s internal thoughts. This prevents bias.
• A librarian checker: Every cited theorem must be quoted exactly and linked clearly; verifiers check that the source exists and matches word-for-word.
• Spotlight the hardest step: The prover must mark the key, original steps and explain them in full detail (no “clearly this holds” allowed).
• Plan first, then execute: On harder problems, one agent writes a structured plan (like a roadmap of subgoals), and another follows it. If something fails, a “Regulator” decides whether to revise the proof, revise the plan, or start a new plan—just like a coach choosing the right fix.
• Two-stage verification: First, a “structural” check ensures the proof solves the exact original problem, uses valid citations, and has a clean subgoal tree. Only then does a “detailed” check go line by line through the math.
• Guard rails on the problem: The system compares the original problem statement word-by-word with what the proof claims to solve, so the question can’t be quietly changed.
• Multiple models in parallel: Different AI models try in parallel; a selector picks the best candidate, reducing the risk of one model’s blind spot.

In short: QED is like a careful, multi-step assembly line for proofs, with quality checks at each station.

What did they find?

They tested QED on five open problems in applied analysis and PDEs (these are math problems about things like fluids and waves, often described by equations that change over space and time). These weren’t homework problems—experts didn’t know the answers beforehand.

• QED produced correct, original proofs for 3 out of 5 problems.
• Independent domain experts checked the proofs and confirmed they were both correct and new (not copied) and required real mathematical insight.

A few highlights:

• For one problem about “mixing” (how a quantity spreads out under certain flows), QED showed that exponential mixing is actually impossible under the given conditions—surprising the expert, who had expected it might be possible.
• For a second problem about the “Batchelor scale” (a special balance point in mixing where advection and diffusion interact), QED proved that a previously known one-way condition is actually an if-and-only-if condition for shear flows. In other words, it upgraded a sufficient condition into a full equivalence—an unexpected and valuable clarification.
• For a third problem about building a special “weight function” to prove powerful inequalities (called Carleman estimates, used for wave equations and inverse problems), QED proposed a function and proof that worked after the experts tightened the requirements. The system adapted and produced a fully valid solution without human hinting on the proof itself.

Why this matters: These are not standard contest problems; they’re genuine research questions. Getting three expert-verified, original proofs is a strong sign that the system design—not just model size—makes the difference.

Why does it matter?

This work suggests a practical way AI can help real math research:

• System design is key: The biggest jump came from organizing the process—separating roles, enforcing source checks, focusing on the hardest steps, and using multi-stage verification.
• Useful partner for researchers: Even when experts don’t know the answer, AI can propose solid candidate proofs or counterexamples. This can guide where humans spend their time.
• Trust through verification: By catching source fabrications, problem changes, and hand-waving, QED builds trust in AI-generated proofs.

If developed further, systems like QED could speed up exploration of new ideas, test conjectures quickly, and help mathematicians zero in on promising directions.

Summary

• Purpose: See if AI can create truly new math proofs, not just solve known problems.
• Approach: A team-like, multi-agent system that plans, proves, and rigorously verifies with strict checks.
• Results: 3 expert-verified original proofs out of 5 open problems, including a surprising impossibility result and a new equivalence.
• Impact: Shows that careful system design can turn strong LLMs into reliable research assistants for real mathematics.

Knowledge gaps, limitations, and open questions

Below is a consolidated list of concrete gaps and unresolved questions left by the paper that future work could address:

• Extremely limited evaluation scope: only five problems in applied analysis/PDEs, with three successes; no evidence of generality to other branches (e.g., number theory, algebraic geometry, combinatorics, logic, topology).
• Selection bias risk: all problems were provided by collaborators; no adversarially chosen or randomly sampled tasks to prevent cherry-picking.
• Missing baselines: no comparisons to single-agent systems, simple self-consistency, tool-augmented agents, or prior open-problem agents under matched conditions.
• No ablation studies: the paper does not quantify which architectural components (e.g., structural vs. detailed verification, citation checks, key-step tagging, regulator) materially drive success.
• Decomposition mode unvalidated: all experiments used simple mode; the decomposer–regulator–retry hierarchy has no empirical evidence of effectiveness on real tasks.
• Multi-model and brainstorm modes largely unused: experiments mainly rely on a single prover per problem; benefits of parallel, diverse model exploration are unquantified.
• Verifier reliability unmeasured: no precision/recall estimates for detecting incorrect proofs; no controlled tests with seeded errors to quantify false accepts/false rejects.
• Lack of adversarial testing: no evaluation against deliberately crafted “proofs” designed to exploit verification blind spots or game <key-original-step> tags.
• No formal verification: all checking is LLM-based over natural language; there is no integration with proof assistants (e.g., Lean/Isabelle/Coq) for machine-checked guarantees.
• Citation-grounding remains opaque: “exact-statement matching” is described, but the paper does not specify robust retrieval/parsing (PDF/LaTeX), canonicalization, or string-level matching tools; empirical accuracy of citation verification is not reported.
• Literature originality check is informal: originality relies on contributor judgment; there is no systematic literature sweep (e.g., cross-archive retrieval, semantic deduplication) or independent external reviewers to reduce the risk of rediscovery.
• Problem-statement integrity checking is brittle: “word-by-word” comparison may miss logically equivalent restatements or subtle constraint shifts; a formal problem DSL and semantic equivalence checks are not provided.
• Key-step tagging effect untested: no evidence that <key-original-step> enforcement reduces hand-waving or misallocated effort in practice; no measurements of tag misuse or verifier sensitivity to mis-tagging.
• No analysis of failures (P1, P2): the paper does not dissect why QED failed, which failure modes dominated, or what modifications would close those gaps.
• Missing resource reporting: runtime, token usage, wall-clock time per round, and cost are not disclosed; scalability and practicality remain unknown.
• Reproducibility risks: reliance on proprietary, evolving models (e.g., “GPT-5.4,” Gemini 3.1 Pro, Claude Opus 4.6) with unspecified prompts, seeds, and decoding parameters hinders repeatability.
• Unclear termination and confidence calibration: criteria for the verdict agent to accept a proof are not quantified; there is no confidence score or risk control for premature acceptance.
• Limited tool use: no integration with CAS (e.g., Mathematica/SymPy), numerical solvers, PDE simulators, or counterexample search to support or refute claims during proof search/verification.
• No long-horizon knowledge accumulation: there is no mechanism to build a reusable lemma library, cross-problem memory, or persistent mathematical ontology to improve over time.
• Handling of diagrams/figures and non-textual arguments is unaddressed: many mathematical proofs require schematic or geometric reasoning beyond plain text.
• Robustness to problem mis-specification: as shown by P5’s constraint revision, there is no automated detection of degenerate or underconstrained formulations or automated tightening of specifications.
• Cross-domain citation coverage and multilingual sources: the system’s ability to validate and interpret non-English or non-arXiv sources is not discussed.
• Sensitivity analysis is missing: impact of hyperparameters (round limits, temperature, sampling width, verifier depth, plan sizes) on success rates remains unknown.
• Pipeline brittleness across long contexts: no evaluation of performance degradation with very long proofs, deep subgoal trees, or complex dependency graphs; retrieval-augmented memory is not explored.
• Ethical/safety considerations for erroneous claims: no protocol for retracting/flagging incorrect “proofs” once disseminated, or for communicating uncertainty to users.
• Publication pipeline and artifacts: full statements/proofs for P5 are withheld; comprehensive release of all proofs, verification reports, prompts, and logs (with stable model versions) would enable community replication.
• Generalization to formalization: open question whether QED outputs can be automatically translated into formal proofs; pathways to hybrid natural-language-to-proof-assistant pipelines are not charted.
• Extending verification coverage: can verifiers detect subtle analytical pitfalls (e.g., Fubini/Tonelli misuse, boundary conditions, domain measurability, regularity losses) reliably without domain-specific checkers?
• Scaling multi-agent diversity: how many models/decoders are optimal before diminishing returns; how to schedule/allocate tokens adaptively based on verification feedback?
• Benchmark design: absence of a public “open-style” benchmark (with hidden solutions) to enable rigorous, scalable evaluation without overburdening human experts.

Immediate Applications

Below are actionable, near-term uses that can be deployed with the current QED system and its components, or with light adaptation.

• Academic mathematics and scientific research (Academia)
  • Use QED as a “proof drafting and vetting” copilot for conjecture triage, preliminary proof attempts, and sanity checks on in-progress papers.
  • Tools/workflows:
  • Standalone verifier as a pre-submission check for problem–proof alignment, subgoal completeness, and citation accuracy.
  • LaTeX/Overleaf plugins that enforce key-original-step tagging and run structural/detailed verification on demand.
  • Assumptions/dependencies: Access to frontier LLM APIs; acceptance of natural-language (non-formal) proof verification; expert oversight for final originality/novelty judgments.
• Journal editorial and peer review support (Publishing/Policy)
  • Integrate structured citation verification and problem-statement integrity checks into manuscript submission pipelines to flag hallucinated references and scope drift.
  • Tools/workflows:
  • “CiteMatch” service that extracts all theorem/lemma citations, checks exact-statement matches, and verifies preconditions.
  • “Claim-Integrity” gate that compares the abstract/main theorem against the proved claim word-by-word.
  • Assumptions/dependencies: Access to the cited sources (open-access or institutional subscriptions); policy decisions on how to handle “Uncertain” verification results.
• STEM education and assessment (Education)
  • Teach proof structure by requiring students to tag <key-original-step> items and submit a verifier report alongside homework/projects.
  • Tools/workflows:
  • LMS integration (e.g., Canvas/Moodle) providing immediate feedback on rigor, vague language detection, and missing subgoals.
  • TA/grader dashboards that prioritize reviewing flagged steps.
  • Assumptions/dependencies: Age-appropriate scaffolding; academic integrity policies for LLM usage.
• Multi-agent coding and software verification pipelines (Software)
  • Adapt the failure-mode-driven design to code generation: separate “builder” and “tester” contexts, enforce “key-complexity” tagging in critical modules, and use a regulator to distinguish “rewrite plan” vs “fix execution.”
  • Tools/workflows:
  • “Code-QED” CI stage: structural checks (requirements coverage, interface contracts, dependency/license validation) followed by detailed tests and static analysis.
  • Multi-model parallel code proposals with selector/verdict agents.
  • Assumptions/dependencies: High-quality test suites; secure sandboxing; cost controls for multi-model runs.
• Model risk management and reporting assurance (Finance)
  • Use problem-modification detection to prevent scope creep in risk/valuation model documentation and regulatory reports; independently verify assumptions and cited results.
  • Tools/workflows:
  • “Assumption Drift Detector” for policy/risk reports that aligns stated assumptions with conclusions and highlights silent changes in quantifiers or domains.
  • Assumptions/dependencies: Domain-specific rules for regulatory standards (e.g., SR 11-7); human sign-off for compliance.
• Verification of PDE-based engineering analyses (Energy, Aerospace, Climate)
  • Check analytical claims, mixing/diffusion estimates, and boundary-condition logic in white papers and design justifications.
  • Tools/workflows:
  • Standalone verifier configured with domain-specific rules (e.g., admissible boundary conditions, parameter ranges, units).
  • Assumptions/dependencies: Availability of the mathematical sections in text; engineering teams willing to adopt structured proof/check artifacts.
• Safety and stability analysis for controllers (Robotics/Autonomous systems)
  • Apply decomposition mode to derive/verify Lyapunov arguments and safety invariants with independent verification stages.
  • Tools/workflows:
  • “Control-QED” templates that force subgoal DAGs (stability conditions, invariance sets, gain bounds) and detailed verification of key steps.
  • Assumptions/dependencies: Clear formalizations of control objectives; integration with simulation for cross-checking.
• Research reproducibility and audit (Cross-sector/Policy)
  • Deploy the verifier as a “scientific audit” tool in institutional repositories to screen for citation hallucinations and misaligned claims in technical reports and preprints.
  • Tools/workflows:
  • Automated batch scanning of new uploads with triage queues for human review of flagged items.
  • Assumptions/dependencies: Institutional buy-in; access to source documents; governance for false positives/negatives.
• Literature survey quality control (Academia/Industry R&D)
  • Use the literature-survey stage plus citation verification to assemble verified mini-surveys for new projects and grant proposals.
  • Tools/workflows:
  • “RefCheck” pipeline that enforces exact-statement matching and source resolution.
  • Assumptions/dependencies: Availability of credible sources; API limits for large-scale scanning.
• Personal learning and drafting aids (Daily life/Education)
  • Students and independent learners can run the standalone verifier to check proofs in notes or blog posts, and to identify exactly where rigor is missing.
  • Tools/workflows:
  • Overleaf/VS Code extensions that flag vague language and missing dependencies in math writeups.
  • Assumptions/dependencies: Internet access for citation checks; responsible-use guidelines in coursework.

Long-Term Applications

These opportunities require further research, scaling, or ecosystem development, but are plausible extensions of the QED architecture and results.

• Natural-language to formal proof pipelines (Academia/Software)
  • Bridge QED’s structured proofs into proof assistants (Lean/Coq/Isabelle) with automated translation of subgoal DAGs and key steps.
  • Potential products: “QED-to-Lean” transpiler; hybrid verifier that pairs natural-language checks with formal proof obligations.
  • Assumptions/dependencies: Advances in semantic alignment and tactic synthesis; robust libraries for target assistants.
• Autonomous scientific discovery loops (Science & Engineering)
  • Combine QED’s decomposition/regulator with experiment design and data analysis agents for closed-loop hypothesis → proof → experiment updates.
  • Potential products: “AI Scientist” platforms for PDEs, materials, or control theory that alternate between analytical proofs and simulations/lab data.
  • Assumptions/dependencies: Reliable tool integration (simulators/lab instruments); safety and oversight frameworks.
• Regulatory-grade verification of scientific claims (Policy/Publishing/Healthcare)
  • Establish standardized, machine-verifiable checklists for clinical, environmental, and safety-critical reports (problem integrity, citations, logical completeness).
  • Potential products: “Reg-Verify” services for FDA/EMA submissions, environmental impact assessments, or safety cases.
  • Assumptions/dependencies: Regulatory acceptance; domain adaptation; traceability and audit logs.
• Certification support for safety-critical systems (Aerospace/Automotive/Robotics)
  • Use structured verification artifacts as part of evidence for certification (e.g., stability proofs, hazard analyses, controller bounds).
  • Potential products: Toolchains that bind decomposition plans and verification reports to requirements and test evidence.
  • Assumptions/dependencies: Alignment with certification standards (DO-178C, ISO 26262); formal-methods integration.
• Large-scale literature integrity scanning (Publishing/Policy)
  • Periodic scanning of archives (e.g., arXiv, institutional repositories) to flag potential citation hallucinations and misaligned claims at scale.
  • Potential products: “SciScan” dashboards for publishers and institutions with trend and risk monitoring.
  • Assumptions/dependencies: Source availability; robust disambiguation of references; handling of paywalled content.
• Domain-optimized proving for applied PDEs and beyond (Energy, Climate, Materials)
  • Extend QED’s success in applied analysis to broader PDE-heavy domains (turbulence, porous media, electromagnetics) and to cross-disciplinary models.
  • Potential products: Libraries of reusable decomposition patterns and domain-specific verification rules.
  • Assumptions/dependencies: Expert-curated rule sets; scalable multi-model orchestration; evaluation benchmarks.
• Enterprise-grade multi-agent orchestration frameworks (Software/IT)
  • Generalize the failure-mode-driven architecture (separation of roles, regulator, two-stage verification, problem-integrity checks) to complex enterprise workflows (e.g., legal drafting, policy analysis, complex systems engineering).
  • Potential products: “Agent Governance” SDKs with built-in failure-mode mitigations.
  • Assumptions/dependencies: Customization for domain semantics; monitoring and cost controls.
• Education at scale with rigorous-feedback tutors (Education)
  • Build tutors that enforce proof structure, detect vague reasoning, and adaptively focus students on key steps, with analytics for educators.
  • Potential products: Courseware integrating auto-verification, skill diagnostics, and formative feedback loops.
  • Assumptions/dependencies: Curriculum alignment; equity and access; privacy protections.
• Novelty detection and credit attribution in math (Academia/Publishing)
  • Pair QED with literature graph mining to assess novelty, prevent rediscovery, and suggest attributions for related results.
  • Potential products: “NoveltyLens” for editors/referees and researchers.
  • Assumptions/dependencies: Comprehensive, structured math corpora; reliable similarity/entailment measures.
• Cross-domain “assumption integrity” guards (Finance/Policy/Analytics)
  • Apply problem-modification checks to prevent hidden assumption changes in forecasts, strategic plans, and analytical dashboards.
  • Potential products: Plugins for BI tools that track assumption→conclusion consistency over versions.
  • Assumptions/dependencies: Access to version histories; standardized assumption capture.

Each application’s feasibility depends on model availability and reliability, cost/performance trade-offs for multi-model runs, domain-specific rule engineering, and governance for human oversight—especially when verification remains in natural language rather than fully formal proof assistants.

• advection--diffusion equation: A partial differential equation combining transport by a flow (advection) with smoothing by diffusion. "Consider the advection--diffusion equation on $\mathbb{T}^2$:"
• Allen-Cahn-Navier-Stokes: A coupled system linking the Allen–Cahn phase-field equation with the Navier–Stokes fluid equations. "Allen-Cahn-Navier-Stokes"
• Batchelor length scale: The smallest scalar-mixing scale in turbulence where diffusion balances advective stretching. "analogous to the Batchelor length scale in turbulence"
• Batchelor scale: A characteristic wavenumber/length at which advection–diffusion dynamics become trapped with persistent balance. "the Batchelor scale should exist with high probability"
• Bessel function: A special function solving Bessel’s differential equation, common in wave and diffusion analyses. "Bessel function analysis"
• Carleman estimate: A weighted inequality used to prove unique continuation, observability, or control properties for PDEs. "to establish a valid Carleman estimate"
• Carleman weight functions: Carefully chosen weight functions satisfying geometric/positivity conditions to enable Carleman estimates. "Carleman weight functions for PDEs."
• chain-of-thought prompting: A prompting method that elicits step-by-step reasoning traces from LLMs. "Chain-of-thought prompting"
• citation hallucination: An LLM failure mode where references or theorem statements are fabricated or misstated. "Citation hallucination"
• context contamination: A verification failure mode where the prover’s reasoning leaks into the verifier, biasing checks. "Context contamination"
• detailed verification: Fine-grained, step-by-step logical and mathematical checking of a proof. "detailed verification (Phase 6)"
• directed acyclic graph (DAG): A directed, cycle-free graph encoding dependencies among subclaims in a proof plan. "a directed acyclic graph (DAG) of intermediate mathematical claims"
• energy cascades: The transfer of energy from large to progressively smaller scales in turbulent flows. "energy cascades in turbulence"
• Erdős conjectures: Open problems attributed to Paul Erdős, often combinatorial or number-theoretic. "700 open Erd\H{o}s conjectures"
• Euler equations: The inviscid (zero-viscosity) PDEs governing incompressible fluid flow. "Euler equations"
• exponential mixing: Rapid (exponential-rate) decay of certain norms of a transported scalar, indicating strong mixing. "exponential mixing is impossible"
• Fourier coefficient: The amplitude of a function’s component at a given frequency in its Fourier series. "the Fourier coefficient $\hat{\theta}(n)$ is given by"
• Fourier-analytic methods: Techniques leveraging Fourier transforms/series to analyze PDEs and mixing. "try Fourier-analytic methods"
• formal proof assistants: Software systems (e.g., Coq, Lean) that check fully formalized mathematical proofs. "formal proof assistants"
• homogeneous H^{-1} norm: A negative-order Sobolev norm measuring distributions via inverse-derivative scaling. "homogeneous $\dot{H}^{-1}$ norm is defined by"
• incompressible flows: Fluid motions with zero divergence (volume-preserving), typical in many PDE models. "incompressible flows"
• L_t^{\infty(W{1,1}_y(\mathbb{T}))}: Functions essentially bounded in time with values in the Sobolev space W^{1,1} in y on the torus. "L_t^{\infty\big(W{1,1}_y(\mathbb{T})\big)"}
• Lebesgue space L²: The space of square-integrable functions on a domain, central to PDE analysis. "L^{2_{x,y}(\mathbb{T}2)"}
• liminf: The limit inferior; the greatest lower bound of all subsequential limits of a sequence/function. "\liminf_{t \to \infty}"
• Navier--Stokes equations: Viscous incompressible fluid PDEs describing momentum and mass conservation. "Navier--Stokes equations"
• partial differential equations (PDEs): Equations involving partial derivatives that model continuum phenomena. "partial differential equations (PDEs)"
• pseudoconvexity: A geometric condition on weights ensuring positivity needed for Carleman estimates. "strict pseudoconvexity-type inequalities"
• shear flows: Flows whose velocity varies in one direction and is directed along a perpendicular axis. "shear flows"
• Sobolev space W^{1,1}: Functions with integrable first derivatives (and the function itself) in L^1. "W^{{1,1}_y(\mathbb{T})"}
• structural verification: High-level proof checks for alignment, completeness, citations, and subgoal structure. "Structural verification"
• subgoal tree: A hierarchical decomposition of a proof into dependent intermediate claims. "Subgoal tree validation."
• transport equation: A PDE describing passive advection of a scalar by a given velocity field. "the transport equation"
• weak solution: A generalized solution satisfying the PDE in an integral/distributional sense. "for the weak solution $\rho$, we have"

Sign up for free to add this paper to one or more collections.