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

The control layer maintains the route pool and budget. It derives quotas for direct, adjacent-domain, and distant-domain routes from the structure of the source problem, receives stress-test results, and decides which bridges stop and which enter more expensive target search. Its state includes the cheapest known rejection test, passed checks, new checkable objects, estimated return cost, and remaining budget. Budget updates require recorded test results or independently checkable evidence rather than narrative assessment alone.

The execution layer performs open-ended work. Generation agents propose proof sketches and bridge opportunities. Retrieval agents locate target mechanisms and theorems. Tool agents call enumeration, computer algebra, SAT/SMT, or field-specific checkers. Lean agents translate statements, retrieve premises, and build candidate proofs. Deterministic programs emit finite witnesses or coverage certificates. Runs use a heterogeneous combination of Claude 4.8, GPT-5.6, and DeepSeek. A single model call is an execution event rather than a separate agent; a role is defined by its permissions, input, and required output.

The verification layer handles objects whose statements are already precise. A target checker establishes whether a target-side claim holds in its target representation. A bridge checker audits direction, assumption differences, preserved structure, and round trips. An independent replayer reruns Lean files or program certificates in an isolated environment. Source-side review substitutes the target result into a fixed return template and decides whether the source statement is resolved. A route proposer cannot certify its own output.

The mathematical-state layer stores two graphs. The task graph records actions, budgets, failures, and recovery points. The claim graph records exact statements, evidence, mathematical dependencies, and versions. Mathematical artifacts and verification records link the two. Completing a target-search task need not create a claim on which later reasoning may depend. Conversely, a local claim may be true without resolving the root problem. Section 4 specifies the update rules.

The interfaces between layers are deliberately narrow. Control schedules only registered routes; execution submits candidates and evidence artifacts; verification issues scoped records; and mathematical state updates nodes from those records. Table 1 lists the input, required output, and state authority for each role.

Every evidence artifact is keyed by $(q_{v},r,b_{v},c_{v})$: the problem version, route, bridge version, and claim version. Revising a bridge creates a new $b_{v}$, so evidence produced for an earlier version does not automatically support the revision. Models can be replaced without changing the mathematical dependency structure.

EULER integrates four capabilities: explicit bridge representations, persistent mathematical state, parallel search, and formal verification. All runs share the same problem version, bridge record, run identifier, and cost definition. Historical case studies and engineering tests do not enter the 120-task evaluation.

This design complements recent mathematical-agent systems. Aletheia and RMA demonstrate long-horizon natural-language research and iterative role assignment (Feng et al., 2026; Zhao et al., 2026). QED links system components to specific failure modes (An et al., 2026). Rethlas/Archon connects informal exploration to Lean verification (Ju et al., 2026). Albilich and Danus provide persistent proof state and fact-graph orchestration, respectively (Gong et al., 2026; Liu et al., 2026). AI Co-Mathematician places related capabilities in an asynchronous research workspace (Zheng et al., 2026a). EULER takes a bridge between mathematical communities as its unit of search and evaluates both the target operation and the evidence returned to the source statement within one experimental design.

Change of representation has also been studied directly. Raggi et al. search for representations that simplify proofs in discrete mathematics (Raggi et al., 2016), while correspondence-based and meta-search methods rank alternative problem representations (Fuentetaja et al., 2018; Stockdill et al., 2020). Translation validation checks that a target computation corresponds to its source instance (Pnueli et al., 1998); counterexample-guided refinement uses failed checks to improve an abstraction (Clarke et al., 2000). Recent work on scalable mathematical discovery similarly treats problem selection and representation as system-level bottlenecks (Zheng et al., 2026b). EULER combines representation choice with an explicit source-return test and measures the two within the same task-level evaluation.

A run begins with $S=(\Gamma_{s},\varphi_{s},v)$, where $\Gamma_{s}$ contains the assumptions, $\varphi_{s}$ is the proposition to prove or refute, and $v$ is the problem version. The system fixes admissible evidence, boundary objects, budget, and stopping rules, then generates a route pool. Each route produces a BridgeOpportunity record. Bridges that pass stress testing enter target search. The verification layer replays submitted artifacts and writes its records to the claim graph. Source-side review then assigns one of six route outcomes: proof, refutation, conditional result, local theorem, bridge rejection, or unresolved. A cost record binds model use, tools, wall time, and expert time to the run identifier.

This flow separates three quantities that are easily conflated. The number of routes is not research progress. Passing a target checker does not establish the original conjecture. A structurally complete verification record does not establish mathematical truth. The controller schedules resources from registered objects; verifiers state exactly what they checked; and only source-side coverage can change the root conclusion.

Each run stores the fixed task definition, mathematical artifacts, verification records, and final source-side outcome under one versioned identifier. This is enough to reconstruct the claim graph from a checked checkpoint; the full storage layout is specified in the appendix.

Let the source problem be $S=(\Gamma_{s},\varphi_{s},v)$, where $\Gamma_{s}$ specifies the object domain and assumptions, $\varphi_{s}$ is the statement to prove or refute, and $v$ fixes the statement version. A candidate bridge is represented by

Here $O_{s}$ and $O_{t}$ are the source and target objects, $f$ is the forward map, and $g$ is an optional return map. The sets $\Delta^{+}$ and $\Delta^{-}$ record added assumptions and omitted source cases, respectively. The set $\mathcal{A}_{t}$ contains the operations made available by the target representation, and $R$ lists the obligations that must be discharged before target-side evidence can support the source statement.

The direction requirements differ for proofs and counterexamples. If the bridge establishes only $s\Rightarrow t$, then $\neg t$ refutes $s$, whereas a proof of $t$ does not in general prove $s$. The bridge record therefore fixes the admissible target result types before search begins. A one-way map cannot be reinterpreted as an equivalence after a result is found.

We write $d(B)$ for the domain distance of a bridge. Before search, annotators score five changes: object type, ambient theory, governing invariant, length of the known correspondence chain, and required expert community. Each change receives a score of 0, 1, or 2. Totals from 0 to 4 define an adjacent-domain bridge, totals from 6 to 10 define a distant-domain bridge, and a total of 5 is excluded from the primary binary comparison. Textual similarity does not enter this judgment, and the eventual success or failure of a bridge does not alter its distance label. Appendix F gives the anchors.

Bridges are ranked by

Here $A$ measures the gain in target-side operations, $K$ the compression of the resulting certificate, and $N$ the absence of the same tool from direct and adjacent-domain routes. The loss term $L$ measures information discarded by the map, $C_{R}$ the cost of returning the evidence, and $C_{D}$ the cost of the early rejection test. Each anchored score from 0 to 4 is divided by 4 before ranking. The primary analysis uses equal coefficients, $\alpha=\beta=\gamma=\lambda=\mu=\nu=1$. The system retains each component score and its justification. Distance $d(B)$ determines only the allocation of route slots across strata.

A route has one of six terminal statuses: the source statement is proved; the source statement is refuted; a conditional result is obtained; a local theorem is obtained; the bridge is rejected by an early test; or the route remains unresolved under the available budget. Target-side artifacts retain their stated scope. For example, a theorem restricted to sparse matrices may enter the claim graph as a local theorem, but it does not change the root status of a conjecture about arbitrary matrices.

Direct routes begin with standard decompositions, known theorems, finite small cases, and natural counterexamples from the source domain. They provide the baseline for bridge-based routes and continually expose boundary conditions and local facts. If a distant-domain bridge ultimately uses the same source lemmas without adding a checker or compressing the certificate, it has only changed the language of the argument.

Adjacent-domain bridges arise from standard representations of the same objects, neighboring invariants, established equivalences, or computational encodings. The two ends usually share some terminology and expert communities, and the forward and return maps are short. Each adjacent-domain bridge must state its gain over the direct route: a shorter certificate, a cheaper checker, a more effective decomposition, or a monotone quantity that is difficult to see in the source representation.

Distant-domain bridges are proposed either by random sampling or by retrieval. Random sampling draws uniformly from a frozen catalog of eligible target mechanisms and measures the value of open-ended analogy by itself. Retrieval ranks the same catalog by a structural fingerprint containing the quantifier pattern, symmetries, local-to-global structure, main obstruction, required evidence type, prospects for finite reduction, and missing operation. The retriever is not given the title, authors, or target answer. For example, an existence problem without a constructive certificate retrieves mechanisms that produce a flow, a matching, an integer-feasible solution, or a finite witness, rather than papers that merely share vocabulary with the source statement.

The three route families start in parallel. Each round preserves at least one direct route, one adjacent-domain bridge, and one distant-domain bridge. The remaining slots are allocated competitively using $U(B)$. This quota prevents safe adjacent-domain routes from consuming the entire budget and prevents domain distance from becoming a reward in its own right.

Constructing a complete map may be too expensive for initial screening. The system first records a BridgeOpportunity, consisting of a structural summary of the source problem, a target mechanism, the expected operation, candidate preserved quantities, obvious losses, an early rejection test, an outline of the return path, and a rough cost estimate. This record is a candidate for budget allocation, not a mathematical claim.

Every score must be tied to a concrete object or test. “The target theory is powerful” is not a justification. “The theory supplies a checker that returns a minimal infeasible subset for $f(x)$” is. Unknown gains receive a score of zero, whereas unknown losses receive the highest risk score. New evidence may update a component, but each update retains the previous value and justification so that rankings cannot be rewritten after the outcome is known.

Candidate bridges first undergo inexpensive structural checks and only later gain access to target-side tools. Figure 3 shows their order, and Table 3 fixes the passing condition and a typical failure for each test.

A direction error or an explicit conflict of assumptions closes the route immediately. When a boundary or round-trip check is inconclusive, the system permits one bounded refinement using a smallest object or a symbolic calculation. An inconclusive tool test triggers only a small paired probe. One arm receives the translated statement; the other receives the same material and one target-native operation, under equal total budgets. When the return test is inconclusive, the target result may be stored as a local artifact but is ineligible for a verified resolution of the source problem.

Translating a natural-language statement into Lean is itself a bridge. The natural-language statement is the source object, the Lean declaration is the target object, the translator supplies $f$, semantic comparison and bidirectional theorems provide the round trip, and the Lean kernel is the target tool. Successful compilation passes only the tool stress test. Quantifiers, scope, degenerate cases, and the direction of return remain subject to the other tests. This view keeps formalization within the same mathematical transfer discipline as every other bridge.

An early rejection test seeks the cheapest witness that decisively invalidates the current bridge. Common tests examine forward and return maps on smallest objects, boundary objects that violate an added assumption, whether the target invariant distinguishes the necessary source cases, the combined length of the target certificate and return argument, and whether the supposedly new target operation already exists in an equivalent form in the source domain. These tests take precedence over long proof searches because a short counterexample can eliminate the remaining cost of an entire distant-domain route.

A failed-route record contains the bridge version, object scope, first decisive stress test, concrete witness, and conditions for reopening the route. The record states that “the map merges positions in sequences with repeated occurrences,” rather than concluding that “the encoding method is invalid.” A route may reopen if it changes the proof-critical map or the object scope. Changing only the model or the wording does not define a new route. Negative results can therefore prevent repeated work without turning a local failure into a judgment about an entire domain.

Surviving bridges receive budget in three stages. The first stage runs small examples, local checkers, or short retrievals. The second searches for target-domain lemmas and certificates. The third permits expensive provers, long retrievals, or formalization. Each stage must add at least one checkable object, such as a decisive counterexample, a reusable lemma, a certificate, a verified map revision, or a more precise description of the obstruction. A route is paused after two consecutive stages without a new object.

The return template is frozen before target-side search. It states which target conclusions suffice to prove the source statement, which suffice only to refute it, and which require separate treatment of exceptional branches. Once a target result is available, its evidence fills the template. Any additional proof-critical step becomes a new source-side subproblem. If the result covers only part of the source domain, the claim graph records a local theorem and the uncovered region.

A verified resolution is the primary endpoint. Target-side validation is a secondary endpoint that records whether the target mechanism produced a valid artifact. Incorrect returns are recorded separately. They occur when a valid target artifact is used to form an invalid source-side conclusion because of direction, scope, or coverage errors.

Budget updates depend on survival under stress testing, the production of new checkable objects, and expected source-side impact. Surviving bridges are ranked in each batch by

where $q(B)$ records the number and verification level of objects added in the current batch, $i_{s}(B)$ estimates their effect on unresolved source-side obligations, and the denominator combines the budget already spent with the current estimated cost of returning the evidence. Explanatory prose does not contribute to $q(B)$. Subject to the route-family quotas and remaining budget, slots are assigned in descending order of $P(B)$.

Route identity is determined by the mathematical mechanism. A boundary counterexample found by an adjacent-domain bridge may close a distant-domain bridge. Conversely, an invariant found through a distant-domain bridge may return to the source side and define a sharper direct route or adjacent-domain bridge. The system records provenance edges whenever material is shared. Two branches that depend on the same critical lemma do not count as independent discoveries. The budget loop retains these transfers without inflating the measured effect through branch proliferation.

The task graph $G_{\mathrm{task}}$ records what to do next. Its nodes represent bridge opportunities, stress tests, target searches, revisions, reviews, and release actions. Its edges encode dependencies, budget release, failure, and recovery. Completing a task means that the artifact specified by its contract has been delivered. For example, an enumeration program may have run and saved its output. Completion alone does not mean that the output supports a mathematical conclusion.

The claim graph $G_{\mathrm{claim}}$ records what is currently known. Its nodes contain frozen source statements, target statements, bridges, lemmas, counterexamples, conditional results, and formal declarations. Its edges represent proof dependencies, refutations, equivalences, specializations, formalization correspondences, and composition relations. Every node is tied to an exact statement, assumptions, a version, and evidence. A change to the statement creates a new version, while existing evidence remains attached to the old version.

Three objects connect the graphs. A candidate submits an execution result to the claim layer. An artifact stores a Lean file, program certificate, target proof, or concrete witness. A verification record states who checked which version, in what environment, and with what result. A successful target-side check may add a target theorem to the claim graph, but the root source statement changes only after the return chain is complete.

A single “verified” flag would collapse several distinct questions. EULER therefore records four evidence axes for each claim. The machine axis covers certificates, kernel checks, and program replay. The semantic axis records the correspondence between natural-language and formal statements. The independent-review axis records blinded judgments and disagreements. The composition axis records whether local lemmas jointly cover their parent claim. Mathematical quality and novelty are tracked separately and do not alter truth status.

Separate axes make genuine intermediate states visible. A Lean file may pass the kernel while formalizing a source statement with narrower scope. A counterexample may be reproduced by two programs before its novelty has been checked for publication. Several local lemmas may each be correct but fail to compose because they use incompatible choices or leave a boundary case uncovered.

Before a local claim can support its parent, the composition axis checks six obligations. Coverage requires the child conclusions to exhaust the parent’s parameter range. Interface compatibility requires the output of one step to satisfy every input condition of the next. Invariant compatibility requires repeated transformations to use the same conventions. Well-foundedness requires an induction or descent to terminate. Joint choice requires separately asserted existential objects to be selectable simultaneously. Boundary coverage requires degenerate cases to be handled outside the generic argument. Table 5 lists common failures.

The composition check produces a coverage table. Each row identifies a parameter region of the parent statement, the child claim responsible for that region, any difference in assumptions, the relevant verification record, and unresolved interfaces. The composition axis records complete closure only when every row is closed and overlapping regions use consistent conventions. If a row is later withdrawn, the affected parent nodes are located directly through the coverage table.

Execution agents may propose claims but cannot change mathematical state directly. A centralized state updater controls admission to the claim graph. A candidate $c$ is admitted when

These predicates check the statement version, object scope, dependencies, evidence, semantic correspondence, and compositional closure. The contract determines which gates apply to each claim type. A finite counterexample may advance after deterministic replay and a check of its assumptions. A general theorem usually requires independent mathematical review, and a formal root conclusion also requires compositional closure.

Verifiers submit verification records rather than writing a claim as “true.” A Lean record states that a particular formal declaration was accepted in a specified environment. A program record states that a given input and concrete output can be replayed. A human record states that an argument passed an agreed checklist. The centralized updater combines these records with the contract and then assigns the claim state. A well-formed record whose provenance cannot be controlled remains supporting evidence but cannot by itself change the root claim.

All verification records share a common format: record identifier, claim version, checker identity, environment, input hash, result code, scope, axioms or external facts used, generated artifacts, and time cost. Each checker adds fields specific to its evidence type. A program record includes input and output summaries; a Lean record includes the declaration name and axiom audit; a human review record identifies the proof-critical steps and the first unresolved gap. This common format lets the controller compare costs without collapsing different kinds of evidence into a single truth value.

The independent verifier recompiles a Lean 4 project (de Moura and Ullrich, 2021) or runs a deterministic checker in an isolated environment. It reads the registered source files, dependencies, tool versions, and inputs, but not the generator’s judgment that the run succeeded. The Lean workflow has three stages: premise retrieval, candidate generation, and independent replay. Retrieval results guide exploration, the generator submits a candidate, and only the replay result enters the machine axis.

Replay also includes an axiom audit. The system checks for sorry, admit, newly introduced axiom declarations, unregistered modules, allowed classical axioms, and the output of #print axioms. Environment failures and mathematical failures receive different codes. A damaged cache or version conflict may be repaired and retried, whereas a type mismatch, missing premise, or construction gap creates a corresponding mathematical task.

The natural-language claim $c_{N}$ and the Lean declaration $c_{L}$ are connected by a separate semantic bridge. Autoformalization systems can generate Lean candidates (Baba et al., 2025; Jana et al., 2026), while round-trip repair and symmetry-aware rewriting test related aspects of translation fidelity (Amrollahi et al., 2026; Olejniczak et al., 2026). Reviewers compare the object domain, parameter range, quantifier order, definitions, additional assumptions, degenerate cases, and conclusion direction. A recent study of 400 graduate-level statements reported an 89.5% compilation rate and a 60.5% consensus faithfulness rate, a difference of 29 percentage points(Zhang et al., 2026). EULER therefore records kernel acceptance and statement faithfulness on separate axes.

Natural-language reviewers read only the frozen objects, permitted artifacts, and review checklist. A local-correctness review identifies the first proof-critical gap. A semantic review compares the achieved result with the contract, while a paper-level review checks how the pieces compose. Two primary reviewers independently assign one of six task-level labels: proved, refuted, conditional, local, unresolved, or incorrect. A third reviewer resolves disagreements. Route-level bridge rejection is recorded separately and does not enter the inter-reviewer agreement calculation.

Bridge failures and claim withdrawals propagate along mathematical dependencies. If a return map fails on a class of objects, source-side conclusions that use that map are withdrawn, while valid local theorems in the target domain remain available. If a target theorem changes its assumptions, only bridges that depend on that version are rechecked. Unrelated parallel routes remain valid.

Each withdrawal records the source node, reason, affected subgraph, and version. A later repair creates new verification records and new composition evidence without overwriting the old record. Recovery reconstructs the task queue, budget, and current claim graph from a frozen checkpoint. This local update preserves expensive target-side artifacts while removing invalid return chains from the root conclusion.

We used the Journal of Combinatorial Theory, Series A (JCTA) only to define an author sampling frame, not as a source of ground truth or a ranking of researchers. JCTA covers finite and discrete structures across several branches of combinatorics and applies a research-level editorial threshold (Elsevier, 2026). A research article in the 24 months preceding the frozen harvest cutoff therefore supplies a coarse external indicator that an author is both recently active and working at a recognized specialist level. This rule avoids a hand-picked list of famous names while retaining subfield diversity. It does not make the resulting cohort representative of all combinatorics or all mathematics.

We collected tasks from publicly available papers written by authors in this 24-month JCTA frame. The collection procedure first extracted statements explicitly marked as a conjecture, question, or problem, then recovered the object domain, quantifiers, parameters, and source of each statement. Statements with the same mathematical content were merged even when their wording differed. A task was eligible if its scope could be fixed before search, proof and refutation had decidable acceptance criteria, the permitted source material was legally accessible, and at least one direct approach could be constructed within the fixed budget.

Eligibility screening was blind to system outcomes. Two curators saw only the statement, publication date, and eligibility fields; they did not see candidate bridges or model attempts. Eligible tasks were stratified by visible structure into four groups of 30: sparse-bridge problems with no mature connection, problems amenable to executable refutation, problems that invited structural transfer, and problems involving natural-language formalization. The strata support balanced analysis, while all aggregate results use the 120 source tasks as the denominator.

Contamination control was completed before retrieval and execution. Famous long-standing conjectures were not used merely because they are difficult: decades of public discussion would make recall and independent discovery difficult to distinguish. The literature index was truncated at the conjecture date, task-level queries masked titles and answer cues published after that date, and model versions were checked against their documented training cutoffs. Exact, paraphrastic, title, and solution-cue overlap screening raised 146 alerts, 23 of which contained substantive information about a solution. We replaced 18 contaminated root tasks and blocked another 5 contaminated routes before freezing the evaluation set. The public ReturnBench-150 set was used to debug the protocol and was not included among the 120 tasks.

Figure 6 begins with 638 papers. The collection procedure extracted 286 candidate conjectures, mathematical deduplication left 214 statements, and eligibility screening produced 120 fixed tasks. The task-level outcome categories are mutually exclusive: 10 proofs, 3 refutations, 27 conditional results, 18 local theorems, 59 unresolved tasks, and 3 incorrect source-side conclusions. The last category records outputs that blinded source-side review rejected; these conclusions were not admitted as verified claims in the claim graph.

The 13 verified resolutions fall into three groups according to their strongest independent check. For 3 tasks, the Lean kernel covered the proof-critical chain. Another 3 were reproduced by an independent implementation of a deterministic program or certificate. The remaining 7 were accepted after separate checks by two mathematicians. The evidence packages also have three release levels. Seven include the statement, routes, artifacts, verification records, and complete source-return chain. Three release the concrete witness and its return chain. Three will be released after the living authors have been notified. Release level does not change the mathematical outcome.

Public human solutions provide a second reference point. Nine tasks received a public human solution during the same time window. In the isolated evaluation, EULER reproduced 4 of them and resolved another 9 tasks for which no solution appeared during that window. The two blinded reviewers obtained Cohen’s $\kappa=0.82$ across the six outcome categories, with a 95% interval of $[0.75,0.89]$. Across five reasoning seeds, the full system resolved 12, 12, 13, 13, and 14 tasks, for a mean of 12.8 and a standard deviation of 0.84.

Each conditional result and local theorem records its exact scope and can serve as a source object in subsequent work, but neither category contributes to the 13 verified resolutions. The 3 incorrect source-side conclusions are also kept separate from execution failures and unresolved tasks. They enter the ablations of stress testing and evidence return directly.

The four structural strata produced different kinds of progress. The executable-refutation stratum resolved 5 tasks, including all 3 counterexamples. The structural-transfer stratum resolved 4 tasks and produced 8 conditional results and 6 local theorems. The language-and-formalization stratum resolved 2 tasks, while 18 remained open. The sparse-bridge stratum resolved 2 tasks and produced 13 conditional or local results.

Both errors in the structural-transfer stratum arose when a valid target theorem was returned with a scope broader than its proof. The error in the sparse-bridge stratum reversed the direction of a map. The language-and-formalization stratum produced no incorrect root conclusion because the semantic evidence axis kept scope-mismatched candidates from changing the root state. The greatest risk therefore arose after target-side evidence had been established but before source-side coverage was complete.

The aggregate results show how often EULER succeeds. The following cases show what a bridge contributes and where an incomplete bridge stops. Figure 7 summarizes each trace as a source problem, a bridge, a target-native operation, and a source-side outcome.

All main experiments use the same 120 fixed source tasks. The statistical unit is the source task: a task contributes one source-level outcome even if it produces several bridges, candidates, or verification records. The primary endpoint is a verified resolution. Secondary endpoints include incorrect source-level conclusions, target-side validations, local results, cost, and human review time. Two reviewers who were blind to the experimental condition labeled each outcome independently, and a three-person panel adjudicated disagreements. We compute 95% percentile intervals from 10,000 nonparametric bootstrap resamples of source tasks and use two-sided exact tests for paired binary endpoints. Means across reasoning seeds are reported with standard deviations.

Figure 8 shows how the experiments fit together. The route-pool comparison measures what each source of routes can resolve. The stress-test experiments measure error filtering. The $2\times 2$ experiment tests whether a bridge changes the available operations. The selector and budget experiments track how resources reach useful routes.

The contamination screen found 23 cases containing substantive answer cues. We replaced 18 root tasks and blocked five routes before execution. Restoring those 23 objects to the candidate pool increased the full-system mean by 2.1 verified resolutions, mostly through title matches and direct clues to known counterexamples. This restoration check shows that contamination was not only a hypothetical concern: admitting the flagged material measurably inflated the endpoint. The main results use the cleaned frozen set.

Nine tasks with public human solutions released in the same window provide a human anchor. The system independently reproduced four of them. The other nine verified resolutions came from tasks with no public solution in that window. The anchor checks task difficulty and the evidence standard; it is not used to rank models against people.

The two blind reviewers agreed on the six outcome classes with Cohen’s $\kappa=0.82$, with a 95% interval of $[0.75,0.89]$. Most disagreements concerned the boundary between conditional results and local theorems. Across the five full-system seeds, the numbers of verified resolutions were 12, 12, 13, 13, and 14, for a mean of 12.8 and a standard deviation of 0.84. The structural-transfer layer had the largest gain, while the formalization layer had the fewest incorrect returns.

The cost ledger records compute cost, tokens, wall-clock time, bridge construction, mathematical review, and state maintenance. Expert time is valued at 200 dollars per hour. Combined task cost is compute cost plus the three categories of human time. For a condition with verified-resolution rate $r$, we define median-normalized cost per verified resolution as the median per-task combined cost divided by $r$. The 552 person-hours of one-time development work are reported separately in the appendix and are not included in the per-task cost.

Three decision thresholds were fixed before the experiments. First, the lower endpoint of the paired interval for the full-system combination comparison against distant-domain retrieval had to exceed zero. Second, the full system had to reduce incorrect returns by at least four relative to the joint pool without bridge-specific tests while retaining at least 12 verified resolutions. Third, the upper endpoint of the median-normalized cost ratio relative to direct search had to be no greater than 1.15. The second threshold was met. The first was not, because the lower endpoint for the resolution difference was $-0.1$ percentage points. The cost ratio was 1.12, with a 95% interval of $[0.91,1.36]$, so the third threshold was also not met.

The experiments support the bridge-specific stress tests and the interaction between bridge material and target-native operations. The full-system combination difference is positive, but its interval crosses zero. Median-normalized cost does not meet the noninferiority threshold. At expert rates of 100, 200, and 400 dollars per hour, the point estimates of the full-system cost ratio relative to direct search are 1.03, 1.12, and 1.21. Reusing the bridge library reduces median bridge-construction time from 36 to 17 minutes per task and lowers the ratio at 200 dollars per hour to 0.99.

The route-pool experiment changes the priority assigned to bridge search. Adjacent-domain bridges resolved nine tasks, and random distant-domain bridges resolved eight; distance by itself did not improve the result. Retrieved distant-domain bridges also resolved eight. The full system reached 13 after adding adjacent-domain routes and bridge-specific tests as part of a larger system combination. Its paired interval still crosses zero, so a larger study should retain the same contract. In practice, the scheduler should first ask which target-side operation becomes available and only then consider how far the target field is from the source field.

Candidate-conditioned replay quantifies the tradeoff between error control and retention. The target checker alone accepted 16 correct and 10 incorrect candidates. The bridge-specific stress test retained 13 correct candidates and reduced incorrect acceptance to three. Strict certification removed the remaining errors but withheld one more correct candidate. Bridge-specific tests therefore serve as the default return rule, with strict certification reserved for root-level claims intended for release and high-risk counterexamples. The targeted tests catch faults in mappings and return chains; applying the strictest rule everywhere would discard mathematics that is already independently checkable.

The $2\times 2$ experiment separates bridge material from target-native operations. Bridge material added 0.8 resolutions when paired with source-native tools, while a target-native operation added 0.6 without bridge material. Together they reached 12.8, yielding an interaction of 4.2 resolved tasks, or 3.5 percentage points. The gain comes from operations native to the target community. The retrieval index should therefore rank algorithms, checkers, representations, and certificate types before theorem titles, and every bridge card should state which new object the target operation can produce.

The selector remains 4.4 resolutions below the post hoc upper bound. Gain-loss ranking uses inexpensive stress tests rather than a one-shot language score. Round-by-round reallocation spends less on rejected bridges and redirects resources to routes that have produced a checkable object. Ranking and allocation use the same feedback, while the recorded failure witnesses filter later retrieval and guide current allocation.

The model and state comparisons address different stages of the system. Heterogeneous model composition improves candidate revision and cross-checking within a run. The two-graph state reduces recovery time, repeated work, and stale returns over longer projects. Bridge identifiers and verification records connect the two, but either component can be replaced and evaluated separately.

The paired resolution and cost thresholds were not met. The incorrect-return threshold was met, and the operation-set interaction point estimate cleared its prespecified threshold. The bridge-library analysis favors reusing verified mappings, scoped failure witnesses, and replayable return templates. These records reduce human work per task while preserving the two mechanism-level gains that were most stable in these experiments.