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

Motivation

• QED targets fully automatic proof generation from human-provided research questions, an area less common than human-guided or closed-system demonstrations.The system is open-source and motivated by the limited reproducibility and autonomy of prior high-profile efforts.Source: §1 · p. 1

Contributions

• QED links seven observed frontier-LLM failure modes to targeted architectural interventions, including separated agents, citation checking, decomposition, and staged verification.These interventions address context contamination, citation hallucination, skipped hard steps, unstable plans, unfocused verification, problem modification, and single-model bottlenecks.Source: §1 · p. 1

Evaluation

• QED independently produced original, nontrivial, complete solutions for 5 of 18 expert-proposed research projects across probability, algebraic geometry, fluid PDEs, and inverse problems.Domain experts independently verified the resulting proofs as original and nontrivial.Source: §1 · p. 2
• Across 214 Codex GPT-5.5 proof candidates, 17 were verifier-accepted and all 17 were accepted by domain experts, yielding 0 observed false positives.This rate was observed under the reported verifier configuration.Source: §1 · p. 2

Scope

• The paper reports selected unsuccessful cases but omits full details for active problems whose human investigation remains ongoing.Many omitted cases are longstanding open problems regarded as genuinely difficult.Source: §1 · p. 2

Evaluation

• Three successful results were assessed as comparable in difficulty and scope to work published in established specialist mathematics journals.The assessment came from collaborating domain experts evaluating the completed solutions.Source: §1 · p. 2

LLM mathematical reasoning

• Open mathematical reasoning benchmarks do not directly establish the ability to produce original research-level proofs, while harder newer evaluations are often closed-source or unavailable.This limits reproducibility and systematic analysis of research-level reasoning.Source: §2 · p. 2

Agent architectures for coding and scientific discovery

• Multi-agent systems increasingly coordinate specialized roles for software engineering and scientific discovery, but QED focuses specifically on mathematical proof generation.QED’s architecture is tailored to mathematical reasoning rather than general workflow coordination.Source: §2 · pp. 2–3
• QED enforces correctness through structured verification of citations, problem-statement integrity, and subgoal-tree consistency.This extends beyond role specialization, conversational refinement, or experimental feedback.Source: §2 · p. 3

AI and open problems

• Unlike several related open-problem efforts, QED is presented as an open-source system producing natural-language proofs for genuinely open problems that experts verified as original.The paper contrasts this with closed systems, rediscovery concerns, and construction-focused results that are not traditional proofs.Source: §2 · p. 3

3.1. Failure Mode 1: Context Contamination

• Shared prover-verifier context or same-model tendencies can bias verification toward accepting flawed arguments.The paper reports that separate calls using the same model still exhibited self-verification bias and more false positives.Source: §3.1 · p. 3

3.2. Failure Mode 2: Citation Hallucination

• LLMs fabricate theorem numbers, attributions, URLs, or source statements, allowing apparently coherent proofs to rely on nonexistent lemmas.The experiments describe citation hallucination as frequent rather than an isolated edge case.Source: §3.2 · p. 3

3.3. Failure Mode 3: Misallocation of Proof Effort

• LLMs often evade difficult original steps with vague language while overexplaining routine components.This leaves the primary novel complexities underexplored.Source: §3.3 · pp. 3–4

3.4. Failure Mode 4: Unstable Proof Plans

• When execution becomes difficult, models frequently abandon their current proof plan and cycle through superficially different strategies.They fail to distinguish a fixable execution error from a fundamentally flawed plan.Source: §3.4 · p. 4

3.5. Failure Mode 5: Unfocused Verification

• A single verifier assigned heterogeneous checks dilutes its attention and can miss critical issues.The affected checks include problem integrity, citations, logical structure, and step-by-step correctness.Source: §3.5 · p. 4

3.6. Failure Mode 6: Problem Modification

• Models sometimes modify quantifiers, assumptions, conclusions, domains, or cases while presenting a proof of the original problem.The resulting proof may be mathematically correct but solve the wrong problem, reflecting proxy optimization.Source: §3.6 · p. 4

3.7. Failure Mode 7: Single-Model Bottleneck

• Different LLMs have distinct mathematical strengths and blind spots, so a single-model system inherits one model’s weaknesses without complementary coverage.The paper motivates multi-model parallel proving and brainstorm mode as a response.Source: §3.7 · p. 4

4.1. Simple Mode

• Simple mode combines literature survey, iterative proof search, independent structural and detailed verification, candidate selection, verdict, and final summarization.Later rounds expose prior proofs and verification results to the prover, while separate verifier invocations avoid shared reasoning context.Source: §4.1 · p. 4
• Multi-model mode generates proofs in parallel and selects among independently verified proof–verification pairs.The architecture can use Claude Code, Codex, and Gemini CLI, with a selector choosing the best candidate.Source: §4.1 · pp. 4–5, Figure 1 · p. 5

4.2. Decomposition Mode

• The decomposition regulator distinguishes execution, plan-level, and strategy-level failures and responds with proof revision, plan revision, or a new decomposition.Configurable limits bound proof attempts, plan revisions, and total decompositions.Source: Table 1 · p. 5, §4.2 · p. 5, Figure 2 · p. 6
• Decomposition mode separates proof planning from execution using a structured plan of quantitative claims, dependencies, difficulty levels, key steps, citations, and self-critique.Six specialized agents include a decomposer, prover, structural verifier, detailed verifier, regulator, and verdict agent.Source: §4.2 · p. 5

4.4. Prover Output Format Enforcement

• Structured prover output requires exact citation information and detailed <key-original-step> tags for nontrivial original reasoning.The verifier flags vague tagged content, missing tags, and inflated tags, forcing attention onto the hardest proof steps.Source: §4.4 · p. 6

4.5. Optional Human-in-the-Loop Steering

• Optional human steering supplies persistent hints or additional verification rules, but it was unused in the open-problem evaluation.The reported evaluation results therefore came without expert guidance during proof generation.Source: §4.5 · pp. 6–7

4.6. Standalone Proof Verifier

• The standalone verifier adapts its depth to problem difficulty, using one streamlined pass for easy problems and structural then detailed agents for hard problems.Detailed verification is skipped when structural verification fails.Source: §4.6 · p. 7

5.1. Experiment Setup

• The evaluation covered 18 research projects contributed by seven experts, with no known proof for any problem at evaluation time.Projects covered probability, operator algebra, algebraic geometry, fluid PDE, and inverse problems.Source: §5 · p. 7, §5.1 · p. 7

5. Experiments

• Full ablations across all projects were omitted because open research lacks benchmark solutions and expert review of each proof is labor-intensive.The study instead used targeted diagnostic ablations on two probability cases, while configuration and retry details varied across projects.Source: §5 · p. 7, §5.1 · pp. 7–8

5.2. Results

• Five of 18 open research projects were solved with original, nontrivial, complete proofs across probability, algebraic geometry, fluid PDEs, and inverse problems.The system operated fully automatically without expert guidance during runs, and the successful proofs were independently reviewed by relevant experts.Source: §5.1 · p. 7

5.1. Experiment Setup

• The five independently solved projects were Projects 6 and 8 in probability, Project 13 in algebraic geometry, Project 15 in fluid PDE, and Project 18 in inverse problems.The successful project records and expert commentary are documented in Appendices A.1–A.5.Source: §5.1 · p. 7, §5.2 · p. 8

5.2. Results

• Three successful results were judged comparable in difficulty and scope to work published in established specialist mathematics venues.The expert assessments included comparisons to venues such as the Electronic Journal of Probability, Proceedings of the American Mathematical Society, Journal of Differential Equations, and Journal of Mathematical Analysis and Applications.Source: §5.2 · p. 8
• Among 214 proof candidates checked with Codex GPT-5.5, 17 were verifier-accepted and all 17 were subsequently accepted by domain experts.No false positives were observed within this verifier configuration and subset.Source: §5.2 · p. 8

6. Discussion

• Five QED proofs were argued to be original because they addressed open questions without domain-expert guidance during proof generation and were characterized as original by experts.The problems were newly proposed by experts in their recent research and had no known solutions.Source: §6 · p. 8
• None of ten single-query GPT-5.5 Pro attempts produced a complete proof for the two probability cases, with every attempt omitting essential steps.The ablations tested whether QED components prevent concrete failure modes rather than estimating a success rate.Source: §6 · pp. 8–9
• Without standardized citation format, proofs misstated theorems or left applications insufficiently explained for verifier checking and expert review.The ablation supports treating citation structure as a correctness and readability constraint rather than a cosmetic format.Source: §6 · p. 9
• Without independent citation verification, one attempt relied on an unpublished research note that readers could not independently verify.Phase 3 therefore checks whether cited sources are public, precise, and usable in the proof, not merely mathematically plausible.Source: §6 · p. 9
• Removing mandatory <key-original-step> tags led the prover to develop an easier lower bound while leaving the harder upper bound as a sketch.The authors interpret tagging and verification as forcing detailed attention to the mathematically novel step.Source: §6 · p. 9
• Simple mode failed to complete either probability question, whereas decomposition mode produced the expert-accepted 20-page and 15-page proofs.The qualitative difference was that decomposition mode maintained a stable plan long enough to resolve difficult upper-bound arguments.Source: §6 · p. 9
• The targeted ablations are limited to two cases and are diagnostic.They do not provide a broad estimate of component-level success rates across the full evaluation.Source: §6 · p. 9

7. Conclusion

• QED produced original, nontrivial proofs for five research projects across probability, algebraic geometry, fluid PDEs, and inverse problems.The system received only problem statements and configuration parameters and ran without human guidance during proof generation.Source: §7 · p. 9
• Three of the five successful results were comparable in difficulty and scope to work commonly published in established specialist mathematics venues.The relevant proofs were subsequently validated by domain experts.Source: §7 · p. 9

A. Successful Projects

• The successful projects and associated public proof records and expert comments are collected in Appendices A.1–A.5 and Table 2.Some items are withheld, as indicated in the appendix proof index.Source: A. Successful Projects · p. 11

A.1. Project 6 — Return Probability Asymptotics for the Lamplighter Walk on Z2 ≀T_d

• Table 2 indexes the appendix proof records for the successful QED projects.The appendix materials include public proof records and expert comments for the successful projects.Source: Table 2 · p. 12
• QED’s Project 6 concerns a sharp return-probability asymptotic for the switch–walk–switch lamplighter walk on Z2 ≀ T_d.The problem studies the return probability p_2n(e,e) after 2n steps on the infinite d-regular tree.Source: §A.1 · pp. 11–12
• Project 6 was solved in decomposition mode after substantial proof-plan refinement, and the resulting proof was verified by the domain expert.The expert described it as a solid specialized probability contribution comparable to work suitable for the Electronic Journal of Probability or Proceedings of the American Mathematical Society.Source: §A.1 · p. 12

A.2. Project 8 — Total Variation Asymptotics for the Switch–Walk–Switch Walk on Z2 ≀Z

• Project 8 concerns a sharp total-variation asymptotic between two laws of the switch–walk–switch walk on Z2 ≀ Z, started from x=(0,0) and y=(0,2).The relation ≍ denotes equality up to positive multiplicative constants independent of t.Source: §A.2 · p. 12
• Project 8 likewise used decomposition mode with substantial proof-plan refinement and was verified by the domain expert.The expert characterized it as a technically nontrivial PhD-level problem in probability theory.Source: §A.2 · p. 12

• QED proved the integral local invariant cycle statement for H1, whereas the classical theorem established only the rational analogue and the integral H2 statement was known to fail.Source: §A.3 · p. 12
• The domain expert supplied only the problem statement, and QED’s proof was independently verified and found mathematically different from the human author’s proof.Source: §A.3 · p. 12
• The proof’s central original idea interprets the coboundary map H1(X∗) → H2(X, X∗) as the residue map, connecting residue theory with Picard–Lefschetz theory for curves.Source: §A.3 · p. 13

• The work establishes explicit, constructive lower bounds for solutions on T2 with mean-zero smooth initial data and divergence-free velocity fields.Source: §A.4 · p. 13
• For inviscid shear, the negative Sobolev norm satisfies ∥θ(t)∥˙H−1 ≥ c∗ 1 + t2 for all t ≥0.Source: §A.4 · p. 13
• For diffusive shear, explicit constants are computable from ρ0, U, and ν, with a uniformly bounded-below mixing scale when 0 < ν ≪1.Source: §A.4 · p. 13
• For sufficiently large A, the advection–diffusion setting admits an explicit threshold A0, exponent cA, and constant C expressed in terms of ρ0, u, L, and ν.Source: §A.4 · p. 13
• The domain expert formulated the problems without intervening in argument construction, and confirmed QED’s complete outputs were correct.Source: §A.4 · p. 13

A.5. Project 18 — Carleman Estimate Weight Functions

• A.5. Project 18 — Carleman Estimate Weight Functions: After experts strengthened weak constraints, QED returned a refined weight function with complete proofs satisfying all conditions.Source: §A.5 · p. 13
• A.5. Project 18 — Carleman Estimate Weight Functions: Experts viewed automated admissible-weight search as a promising application because valid weights require operator-, geometry-, boundary-, and pseudoconvexity-specific adaptation.Source: §A.5 · pp. 13–14

B. Unsuccessful Cases

• B. Unsuccessful Cases: QED attempted additional problems but did not solve them within its preset budget, and the cases were retained for future evaluation.Source: B. Unsuccessful Cases · p. 14

B.1. Project 2

• B.1. Project 2: The open problem asks whether the Aut(Td)-invariant proper edge-coloring measure on a d-regular tree is a factor of i.i.d.Source: §B.1 · p. 14

B.2. Project 3

• B.2. Project 3: The problem asks whether every Aut(Td)-invariant finitely dependent measure on a finite-state process over Td is a factor of i.i.d.Source: §B.2 · p. 14

B.3. Project 7

• B.3. Project 7: The attempted problem asks whether the expected distance d3(n) of a three-dimensional self-avoiding walk grows faster than n1/2.Source: §B.3 · p. 14

B.4. Project 10

• Project 10 considers zero-temperature Glauber dynamics on the infinite 4-regular tree with i.i.d. initial spins and parameter p.The problem asks to prove Morris’ conjecture for this process.Source: §B.4 · p. 14
• For every p > 1/2, the process fixates to +1 at every vertex almost surely under zero-temperature Glauber dynamics on T4.The dynamics updates each vertex toward the majority of its four neighbors, with uniform randomization in ties.Source: §B.4 · p. 14

B.5. Project 11

• Project 11 asks whether coarse embeddability is preserved when countable discrete groups have isomorphic group von Neumann algebras.The question is whether coarse embeddability of Γ implies coarse embeddability of Λ when LΓ ≃ LΛ.Source: §B.5 · p. 15

C. Retry Information

• Table 5 indexes simple or legacy-mode QED runs according to their verification rounds.Source: Table 5 · p. 15
• In decomposition mode, an attempt generates a new plan, revisions regenerate a proof under the same plan, and proof number counts modifications of that proof.Some successful appendix entries contain multiple internal problem statements, and not every one necessarily appears in the final proof.Source: Table 4 · p. 15