← All papers
First page of EULER: Exploring Underused Links with Evidence-Checked Return for Multi-Agent Mathematical Discovery

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

Ren Zhenzhuo

cs.AI Aug 28, 2026 · v1 cs.MA
Multi-agent mathematical discovery system whose Lean agents translate statements, retrieve premises, build proofs, and independently replay Lean 4 projects for verification.
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.

Moving a mathematical problem from one community's objects and tools to another's can help solve it, but such transfers are costly to build and check, so they are often skipped. The goal is to automate this cross-domain bridging while keeping every conclusion validly tied back to the original conjecture.

EULER runs direct, adjacent-domain, and distant-domain routes in competition around a fixed conjecture. A bridge keeps its budget only if it adds an operation the source representation cannot execute and its evidence returns to the source statement along a checked implication. Six ordered stress tests (direction, assumptions, boundary, round trip, tool, and others) reject invalid bridges before expensive search. Lean agents translate statements, retrieve premises, and generate proofs; an independent replayer recompiles Lean 4 projects and audits axioms; task and claim graphs keep versioned evidence records.

On 120 recent combinatorics conjectures from authors publishing in JCTA, EULER produced 10 proofs, 3 refutations, 27 conditional results, and 18 local theorems, with 3 incorrect conclusions. Bridge-specific stress tests cut incorrect conclusions from 9 to 3. Combining bridge material with a target-native operation gave a positive interaction of +4.2 resolved tasks.

OutcomeCountShare
Proved108.3%
Refuted32.5%
Conditional result2722.5%
Local theorem1815.0%
Unresolved5949.2%
Incorrect source conclusion32.5%
Source-level outcomes on 120 conjectures