# EULER: Exploring Underused Links with Evidence-Checked Return for Multi-Agent Mathematical Discovery

arXiv: https://arxiv.org/abs/2609.00032 · HTML: https://mlsanity.com/paper/2609.00032/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 13 of its 24 references that are in the map.
- First posted on arXiv 28 Aug 2026.

## Builds on (most cited first, 13 of 13)

- [Towards Autonomous Mathematics Research](https://mlsanity.com/paper/2602.10177/) (2026)
- [Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs](https://mlsanity.com/paper/2506.19923/) (2025)
- [Automated Conjecture Resolution with Formal Verification](https://mlsanity.com/paper/2604.03789/) (2026)
- [ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings](https://mlsanity.com/paper/2510.15681/) (2025)
- [AI co-mathematician: Accelerating mathematicians with agentic AI](https://mlsanity.com/paper/2605.06651/) (2026)
- [QED: An Open-Source Multi-Agent System for Generating Mathematical Proofs on Open Problems](https://mlsanity.com/paper/2604.24021/) (2026)
- [Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization](https://mlsanity.com/paper/2606.31002/) (2026)
- [Faithful Autoformalization via Roundtrip Verification and Repair](https://mlsanity.com/paper/2604.25031/) (2026)
- [Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory](https://mlsanity.com/paper/2607.06447/) (2026)
- [RMA: an Agentic System for Research-Level Mathematical Problems](https://mlsanity.com/paper/2605.22875/) (2026)
- [Albilich: Steerable Proof-State Orchestration for LLM-Based Mathematical Research with CAS Integration](https://mlsanity.com/paper/2607.27705/) (2026)
- [The Problem Is the Problem: Towards Scalable Mathematical Discovery](https://mlsanity.com/paper/2608.16977/) (2026)
- [What are the Right Symmetries for Formal Theorem Proving?](https://mlsanity.com/paper/2605.22257/) (2026)

## Abstract (arXiv)

Mathematical communities work with different objects, invariants, and tools, so transferring a problem across them is expensive and often skipped. We present EULER, a multi-agent system that takes such a transfer--a bridge--as its unit of search. Around a fixed conjecture, EULER runs direct, adjacent-domain, and distant-domain routes in competition; a bridge keeps its budget only if it supplies an operation the source representation cannot execute and its target-side evidence returns to the original statement along a checked implication. Six ordered stress tests reject invalid bridges before expensive search begins. We evaluate EULER on 120 recent conjectures. The conjectures were frozen before search and screened for contamination, and are drawn from public papers by authors who had recently published in the Journal of Combinatorial Theory, Series A, a leading journal in combinatorics. EULER produced 10 proofs and 3 refutations, plus 45 scoped partial results. Two mechanisms held up under ablation: bridge-specific stress tests cut incorrect conclusions from 9 to 3, and bridge material combined with a target-native operation yielded a positive interaction of +4.2 resolved tasks that neither factor produced alone. Domain distance did not reliably predict success; executable operation gain and valid return did.