Danus uses a main planner, parallel workers, and a shared verified fact graph to construct long research-level mathematical proofs across six case studies.
QED: An Open-Source Multi-Agent System for Generating Mathematical Proofs on Open Problems
2 Pith papers cite this work. Polarity classification is still indexing.
2
Pith papers citing it
abstract
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.
years
2026 2representative citing papers
Sharp return probability asymptotic p_{2n}(e,e) = ρ_d^{2n} exp[−(π²(log(d−1))² + o(1)) n / log² n] for the switch-walk-switch lamplighter walk with Z_2 lamps on the infinite d-regular tree, with proofs generated by the QED AI system.
citing papers explorer
-
Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory
Danus uses a main planner, parallel workers, and a shared verified fact graph to construct long research-level mathematical proofs across six case studies.
-
Return Probability for the Switch--Walk--Switch Lamplighter Walk on a Regular Tree
Sharp return probability asymptotic p_{2n}(e,e) = ρ_d^{2n} exp[−(π²(log(d−1))² + o(1)) n / log² n] for the switch-walk-switch lamplighter walk with Z_2 lamps on the infinite d-regular tree, with proofs generated by the QED AI system.