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

Ren Zhenzhuo

cs.AIAug 28, 2026

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

Authors: Ren Zhenzhuo

Abstract

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.

Figures & tables

Panel of Figure 1 — Figure 1: Adjacent-domain and distant-domain bridges connect the source problem to target-native operations. Stress testing and source-side return determine whether target evidence changes the source outcome.

Panel of Figure 2 — Figure 2: One EULER research cycle. The middle row follows the mathematical workflow, the control layer allocates resources, and the state layer stores tasks, dependencies, and verification records.

Role	Reads	Must deliver	State authority
Controller	Fixed task definition, route pool, verification records, costs	Next task, budget, and stopping reason	Queues and quotas in the task graph
Exploration worker	Source statement, allowed material, failure records	Bridge card, proof sketch, or counterexample candidate	Candidate creation only
Target checker	Target statement, artifact, and environment	Target-side validation record	Target-evidence axis
Bridge checker	Map, assumption differences, return template	Preservation result, counterexample, or open obligation	Bridge state and dependency edges
Independent replayer	Registered artifact, dependencies, tool version	Reproducible output, axiom list, and error class	Machine-evidence axis
Source reviewer	Fixed statement, bridge records, target evidence	Coverage table, source verdict, and scope	Root-conclusion candidate

Table 1: Inputs, required outputs, and state authority of the core roles

Signal	Question	Checkable justification
$A$ operation gain	What can the target domain do that the source route cannot	Interface to a checker, exact algorithm, strong invariant, or established theorem
$K$ certificate compression	Is the target certificate, including its return path, shorter	Certificate size, number of obligation nodes, and independent checking steps
$N$ tool absence	Does the source side already provide an equivalent operation	Tool inventories for direct and adjacent-domain routes
$L$ mapping loss	What structure disappears in translation	Failure of injectivity or surjectivity, parameter merging, and omitted objects
$C_{R}$ return cost	How does the target result support the source statement	Return steps, open branches, and required expertise
$C_{D}$ rejection cost	What is the cheapest decisive test	A smallest case, boundary case, round-trip check, or dimensional check

Table 2: Ranking signals and required justifications for a bridge opportunity

Panel of Figure 3 — Figure 3: The six stress tests are ordered by cost. Direction, assumption, and boundary checks reject invalid routes before deep search; tool and return checks determine whether target evidence can support the source statement.

Stress test	Passing condition	Typical failure
Direction	The target result supports the required source conclusion along the registered implication	Using $s\Rightarrow t$ to treat a proof of $t$ as a proof of $s$
Assumptions	Every target assumption follows from $\Gamma_{s}$ or is proved separately	Hiding positive definiteness, finiteness, general position, or another condition inside a definition
Boundary	The map remains in scope on smallest, degenerate, and extreme objects	Failure at the zero object, low dimension, a parity change, or a dimension jump
Round trip	$g(f(x))$ recovers the structure used by the source conclusion	Merging two source objects that the argument must distinguish
Tool	$\mathcal{A}_{t}$ supplies an executable operation absent from source routes	Rephrasing the problem without adding a checker or theorem interface
Return	Filling the frozen return template covers $\varphi_{s}$	Leaving an exceptional branch, a joint choice, or a parent-level composition step unresolved

Table 3: Passing conditions and typical failures for the six stress tests

Panel of Figure 4 — Figure 4: Feedback-based budget allocation. Routes that survive stress testing and produce checkable objects continue to receive resources. Failed routes retain a scoped witness and reopen only after the map, target mechanism, or return relation changes.

Panel of Figure 5 — Figure 5: The task and claim graphs store different relations. The task graph represents execution order and resource dependencies; the claim graph represents mathematical content and evidence coverage. Candidates, artifacts, and verification records connect the two.

Evidence axis	Central question	Typical states
Machine	Can an explicit object be replayed by an independent checker	Unchecked, certificate accepted, kernel accepted, replay failed
Semantic	Does the formal or target statement faithfully express the source statement	Unchecked, scope in question, human confirmed, mechanically equivalent
Independent review	Do independent reviewers accept the proof-critical argument	Unreviewed, revision required, accepted, disagreement
Composition	Do the local results jointly imply the parent claim	Local leaf, partial closure, closure complete, withdrawn

Table 4: Questions answered by the four evidence axes

Obligation	Relation to check	Common failure
Parameter coverage	The union of the child scopes covers the parent statement	A sparse case is presented as the general case
Interface compatibility	Each output satisfies every assumption of the next lemma	Confusing quotient objects, sequences, and sets
Invariant compatibility	Group operations, lengths, and sign conventions agree across maps	Switching between left and right actions or counting conventions
Well-founded descent	Every recursive step strictly decreases the frozen measure	A cyclic dependency or a zero-step descent
Joint choice	Local existential claims can be realized by the same object	Combining separate existence claims into simultaneous existence
Boundary coverage	Smallest, degenerate, and extreme parameters close separately	Division, nonemptiness, or invertibility fails at the boundary

Table 5: Six obligations for compositional closure

Panel of Figure 6 — Figure 6: Dataset-construction funnel and mutually exclusive outcomes for the cleaned frozen set. The 120 tasks were retained after 18 contaminated root tasks were replaced and five contaminated routes were blocked. Among them, 10 ended in proofs and 3 in counterexamples; conditional results, local theorems, and unresolved tasks formed the majority.

Outcome	Count	Share	Admission criterion
Proved	10	8.3%	An independently reviewed proof chain covers the fixed statement
Refuted	3	2.5%	A concrete object satisfies every premise and violates the conclusion
Conditional result	27	22.5%	Additional assumptions are explicit and the conclusion is proved under them
Local theorem	18	15.0%	The result covers a proper subclass or a finite parameter range
Unresolved	59	49.2%	No valid conclusion on the full source problem is available at the budget limit
Incorrect source conclusion	3	2.5%	The target artifact is valid, but its return direction or coverage is wrong

Table 6: Source-side outcomes and strongest evidence for the 120 eligible tasks

Structural stratum	Verified	Conditional	Local	Unresolved	Incorrect	Total
Sparse bridge	2	8	5	14	1	30
Executable refutation	5	5	3	17	0	30
Structural transfer	4	8	6	10	2	30
Language and formalization	2	6	4	18	0	30
Total	13	27	18	59	3	120

Table 7: Mutually exclusive source-side outcomes in the four structural strata

Panel of Figure 7 — Figure 7: The three traces end in a counterexample, a local theorem, and a partial formalization with an open obligation.

Case	Bridge type	New operation	Decisive stress test	Source-side outcome
Zhao	Distant-domain computation	Occurrence encoding and exhaustive enumeration	Encoding fidelity, length bounds, and witness return	Counterexample
AJT(5)	Adjacent-domain structure	Support-graph decomposition and transfer counting	Scope of dense rows	All-dimensional local theorem
Gao	Multi-bridge composition	Zero-sum tools, descent, and Lean	Parameter coverage, joint choice, and semantic correspondence	Candidate theorem with partial formalization

Table 8: Bridges, operations, decisive stress tests, and outcomes in the three cases

Panel of Figure 8 — Figure 8: Four ablation families separate route supply, stress-test behavior, target-side operations, and resource allocation.

Strategy	Verified resolutions	Incorrect conclusions	Other outcomes	Target-side validations
Direct search	8	4	108	–
Adjacent-domain bridges	9	3	108	15
Random distant-domain bridges	8	4	108	18
Retrieved distant-domain bridges	8	3	109	20
Joint bridge pool, no bridge-specific tests	12	9	99	27
Full system	13	3	104	26

Table 9: Route-pool outcomes. The first three source-level columns sum to 120; other outcomes include conditional results, local theorems, and unresolved tasks

Panel of Figure 9 — Figure 9: Verified resolutions and incorrect source-side conclusions for six route pools. The combined pool increases both counts; adding bridge-specific stress tests preserves 13 resolutions and reduces incorrect conclusions to 3.

Return rule	Correctly accepted	Incorrectly accepted	Withheld
Target checker only	16	10	0
Matched-information generic stress test	15	6	5
Bridge-specific stress test	13	3	10
Strict certification	12	0	14

Table 10: Candidate-conditioned replay of 26 target-side validations

First decisive outcome	Adjacent-domain bridge	Distant-domain bridge
Direction mismatch	16	27
Unmet added assumption	13	25
Boundary or round-trip failure	19	24
No gain from a target-native operation	31	13
Return cost too high	13	10
Passed and entered deep search	18	15

Table 11: First decisive outcome for 240 preselected bridges. Each column sums to 120

	Source-native tool interface	Target-native operation
No bridge material	7.2	7.8
Bridge material	8.0	12.8

Table 12:

2\times 2

results for bridge material and target-native operations. Values are five-seed means of verified resolutions out of 120 tasks

Selector	Mean verified resolutions /120	Seed standard deviation
Semantic similarity	7.4	0.9
Early rejection cost	8.1	0.8
Uniform selection	8.6	1.0
Automated representation meta-search	9.8	0.8
Correspondence recommendation	10.7	0.7
Gain-loss ranking	12.8	0.8

Table 13: Selector results on a fixed pool of eligible bridges

Budget rule	Verified resolutions	Incorrect returns	Rejected-bridge budget	Normalized cost ratio
Even adjacent/distant split	10	5	32%	1.39
Fixed $2{:}1$ adjacent preference	10	4	28%	1.34
One-shot first-round $U(B)$ allocation	11	4	24%	1.26
Round-by-round stress-test feedback	13	3	17%	1.12

Table 14: Budget-rule ablation

Model condition	Mean verified resolutions	Mean incorrect returns	Compute cost/task
Model A	10.2	4.2	486
Model B	9.8	3.8	482
Model C	8.9	4.6	477
Homogeneous multi-agent	11.1	3.7	484
Heterogeneous composition	12.8	3.0	485

Table 15: Model composition under matched cost caps

Panel of Figure 10 — Figure 10: Model compositions under matched cost caps. The heterogeneous configuration has the highest mean number of verified resolutions; Table 15 gives the corresponding error counts and costs.

Strategy	Compute cost	Million tokens	Wall-clock hours	Bridge min	Math review min	State min	Combined cost/task	Normalized cost/resolution
Direct search	170	2.6	3.1	0	31	12	313	4695
Adjacent-domain bridges	187	2.9	3.6	18	36	14	414	5520
Random distant-domain bridges	214	3.3	4.2	31	43	15	511	7665
Retrieved distant-domain bridges	225	3.4	4.4	29	45	16	525	7875
Full system	238	3.6	4.8	36	44	19	568	5243

Table 16: Median per-task cost and median-normalized cost per verified resolution

Appendix figures & tables13 assets

Supplementary material from the paper’s appendix.

Appendix

Field	Content
Exact statement	Object domain, quantifiers, parameters, conclusion, and statement version
Exact negation	Premises a counterexample must satisfy and the conclusion it must violate
Admissible evidence	Natural-language proof, concrete witness, formal proof, program certificate, or a combination
Boundary set	Minimal, degenerate, extreme, and first nontrivial cases
Source-side decision	Operational definitions of the six mutually exclusive outcomes
Contamination cutoff	Conjecture date, retrieval cutoff, and admissible document versions

Appendix

Table 17: Fields fixed for each source task

Field	Content
Identity	Task version, route identifier, bridge family, bridge version, proposer, and time
Source and target	Object types, statements, parameters, encodings, and mathematical communities
Maps	$f$ , candidate back-map $g$ , direction, domain, and exceptional set
Preservation relation	Invariants, order, invertibility, counts, or semantic correspondence
Target mechanism	New operation supplied by a theorem, algorithm, verification procedure, or representation
Source-return contract	Required certificate, covered region, and composition interface on the source side

Appendix

Table 18: Core fields of a BridgeOpportunity record

Candidate source	Main retrieval signal	Required object	Check before stress testing
Direct route	Source terminology, theorem neighborhood, and standard reductions	Source-side proof or counterexample plan	Same scope as the fixed statement
Adjacent-domain bridge	Shared objects, classical associated quantities, and standard functors	Explicit map and an adjacent-domain mechanism	At least one preserved quantity
Distant-domain random	Eligible random sample from the target-mechanism catalog	Explicit object transformation	Interpretable direction and executable target operation
Distant-domain retrieval	Structural fingerprint, certificate type, and new operation	Map, target mechanism, and source-return sketch	Operation not duplicated in the direct pool
Expert proposal	Expertise spanning two domains and known failure patterns	Reviewable bridge record	Complete source, scope, and reviewer fields
Formalization route	Statement structure, library lemmas, and decidable fragments	Semantic map and Lean goal	Registered environment, quantifiers, and permitted axioms

Appendix

Table 19: Generation signals and eligibility checks for route candidates

Code	Recorded fact	Valid reopening condition
DIR	The target conclusion has the wrong direction for the required source conclusion	Replace the target theorem or use a valid converse
ASM	The target mechanism requires an assumption absent from the source problem	Prove the assumption, state a conditional result, or replace the bridge
BND	A minimal, degenerate, or extreme object violates the map	Restrict the scope and handle the failed region separately
RT	The round trip loses proof-critical structure or merges distinct source objects	Change the encoding, add identifiers, or revise the source return
ACT	A matched-budget probe produces no new operation	Use a different target mechanism
RET	The target evidence does not cover the fixed source statement	Add a coverage lemma or change the source-side outcome

Appendix

Table 20: Failure codes, mathematical meaning, and reopening conditions

Directory	Main files	Reproducible check
contracts/	Fixed statement, exact negation, boundaries, and evidence contract	Check the denominator and statement version
routes/	Bridge records, route lineage, retrieval sources, and failure ledger	Reconstruct the candidate pool and route identities
stress_tests/	Six stress-test records, object witnesses, and costs	Recompute the survival funnel and stopping decisions
artifacts/	Proofs, counterexamples, programs, Lean files, and output summaries	Check the mathematical objects independently
verification/	Target, bridge, replay, semantic, and source-side verification records	Check evidence scope and composition
outcomes/	Six outcome categories, blinded decisions, and release tiers	Reconstruct primary and error endpoints

Appendix

Table 21: Directories and review entry points in the reproducibility bundle

Dimension	Score 0	Score 1	Score 2
Object type	Same object and encoding	Standard derived object or specialization	Changed object type and combinatorial structure
Theory	Same theory	Standard adjacent branch	Different basic definitions and theorem system
Governing invariant	Original invariant retained	Classical associated quantity	New governing invariant
Correspondence length	One standard equivalence	Two or three established steps	New composition of maps required
Expert community	Complete review within one domain	Joint review by adjacent domains	Primary review by another community

Appendix

Table 22: Five-dimensional anchors for bridge distance

Component	Score 0	Score 2	Score 4
$A$	No new operation	New verification procedure or local algorithm	Decisive algorithm, strong invariant, or proof interface
$K$	No reduction in evidence length	Some obligations are compressed	Target certificate plus return is substantially shorter
$N$	An equivalent tool exists in the source routes	The source tools can simulate it only indirectly	Neither the direct nor adjacent-domain pool has a comparable operation
$L$	All proof-critical structure is preserved	Exceptions or merged objects can be enumerated	The map loses structure required by the source conclusion
$C_{R}$	One standard source-return step	Several local obligations are needed	Source return nearly repeats the original proof
$C_{D}$	A small example decides the route	A local program or expert check is required	Cost approaches that of a complete target proof

Appendix

Table 23: Anchors for the six bridge-utility components on the 0 to 4 scale

Type	Fixed input	Preferred test	Output object
Direction	$s,t$ and required result type	Implication direction and contrapositive	Valid result direction or reverse task
Assumption	$\Gamma_{s}$ , target premises, and $\Delta^{+}$	Premise difference and missing-assumption witness	New subproblem or conflicting object
Boundary	Minimal, degenerate, and extreme objects	Low-order enumeration and symbolic boundaries	Boundary certificate or counterexample
Round trip	$f,g$ and preserved quantities	Compare $g(f(x))$ and invariants	Preservation proof or information loss
Operation	$\mathcal{A}_{t}$ and source-tool inventory	Matched-budget paired probe	New operation and incremental artifact
Source return	Fixed source-return template	Obligation filling and coverage check	Source-side chain or open branch

Appendix

Table 24: Operational template for bridge-specific stress tests

Condition	Direct	Adjacent pool	Distant pool	Retrieval	Target operation	Specific tests	Source-return rule
Direct search	1	0	0	0	0	0	Direct source-side review
Adjacent-domain bridges	1	1	0	0	1	0	General source return
Distant-domain random	1	0	1	0	1	0	General source return
Distant-domain retrieval	1	0	1	1	1	0	General source return
Combined, no specific tests	1	1	1	1	1	0	General source return
Full system	1	1	1	1	1	1	Bridge-specific source return

Appendix

Table 25: Capabilities and source-return rules in the route-pool conditions

	Distant retrieval resolved	Distant retrieval unresolved	Total
Full system resolved	7	6	13
Full system unresolved	1	106	107
Total	8	112	120

Appendix

Table 26: Paired outcomes for the full system and distant-domain retrieval

Audit stage	Count	Decision and recorded evidence
Overlap alert	146	Retain the matched text, date, version, query, and alert type for curator review
Substantive answer cue	23	Record the proof idea, counterexample clue, answer-bearing theorem, or query shortcut
Root-task contamination	18	Remove the task before execution and link it to a same-stratum replacement
Route-level contamination	5	Keep the root task but block the affected route and its answer-bearing material
Restoration check	23	Reinsert only for sensitivity analysis; the full-system mean rises by 2.1 verified resolutions

Appendix

Table 27: Contamination decisions made before the evaluation set was frozen

Field	Content
Declaration identity	Claim identifier, statement version, Lean name, and source file
Environment	Lean, Mathlib, project dependencies, execution policy, and imports
Result	Compilation status, error category, runtime, and resource limit
Axiom audit	sorry / admit , new axioms, unsafe , and #print axioms
Semantic edge	Correspondence of natural-language objects, quantifiers, scope, degenerate cases, and direction
Composition edge	Parent claim, dependency subgraph, open obligations, and covered range

Appendix

Table 28: Required fields in a Lean verification record

State condition	Repeated target runs	Stale returns	Recovery minutes	Unrelated withdrawals
No persistent state	29	7	93	25
Task graph only	13	4	56	14
Task and claim graphs	4	0	34	5

Appendix

Table 29: State experiment after three recoveries and two version changes

Explore similar work

Mar 4, 2026

Discovering mathematical concepts through a multi-agent system

Mathematical concepts emerge through an interplay of processes, including experimentation, efforts at proof, and counterexamples. In this paper, we present a new multi-agent model for computational mathematical discovery based on this observation. Our system, conceived with research in mind, poses its own conjectures and then attempts to prove them, making decisions informed by this feedback and an evolving data distribution. Inspired by the history of Euler's conjecture for polyhedra and an open challenge in the literature, we benchmark with the task of autonomously recovering the concept of homology from polyhedral data and knowledge of linear algebra. Our system completes this learning problem. Most importantly, the experiments are ablations, statistically testing the value of the complete dynamic and controlling for experimental setup. They support our main claim: that the optimisation of the right combination of local processes can lead to surprisingly well-aligned notions of mathematical interestingness.

Daattavya Aggarwal, Oisin Kim, Carl Henrik Ek +1

Department of Computer Science and Technology, University of Cambridge.

Autonomous Scientific Discovery Mathematical Reasoning Multi-Agent Systems Multi-Agent Reasoning

Ask PDF

Apr 27, 2026

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

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.

Chenyang An, Qihao Ye, Minghao Pan +1

University of California, San Diego, La Jolla, USA · California Institute of Technology, Pasadena, USA · Amazon Web Services

AI Agents for Scientific Discovery Automated Theorem Proving Multi-Agent Reasoning LLM Mathematical Reasoning

Ask PDF

Oct 4, 2026

EPOCH: Reliable Discovery through Evidence-Governed Search

AI research agents are increasingly used to search over programs, mathematical constructions, and proofs. However, existing systems typically optimize evaluator feedback without adequately governing how that feedback is interpreted, challenged, and reused. As a result, promising but fragile candidates can be promoted as discoveries, while benchmark improvements, finite certificates, and theorem-level claims are too easily conflated. We introduce EPOCH, an evidence-governed architecture designed to close this gap. EPOCH implements an evidence-governed discovery loop by combining explicit task contracts, typed memory, active falsification, admission checks, and independent replay, so that each candidate is evaluated against the strength and scope of the claim it supports. EPOCH achieves state-of-the-art aggregate performance on AlgoTune, substantially exceeding the strongest baseline in mean normalized score (0.65 vs. 0.53), and attains the highest mean score on the internal Math14 suite (0.57). It further shows favorable held-out behavior under official-test replay and leads the descriptive aggregate on AgentHPO. Across ten discovery problems, EPOCH delivers substantial task-specific advances, including improved executable constructions, optimized algorithms, counterexamples, and proof-supported results. These advances demonstrate its ability to convert search into concrete progress across mathematical and computational domains. Together, the results suggest that evidence governance is a necessary step toward AI research agents that produce not only stronger solutions, but also more trustworthy scientific discoveries.

Binjie Guo, Aisheng Mo, Ruitong Li +1

Zhejiang University · The University of Hong Kong

AI Agents for Scientific Discovery Autonomous Research Agents Automated Algorithm Discovery

Ask PDF