PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Ren Zhenzhuo

arXiv:2609.00032v1cs.AIcs.MA

TL;DR

Cross-community mathematical transfers are costly because different fields use different objects, invariants, tools, and evidence standards. EULER searches such transfers as validated bridges within a multi-agent system, and its evaluation finds safer returns and a positive interaction between bridge material and target-native operations, with scope and residual-contamination limits.

  • Problem

    Transfers across mathematical communities are expensive to construct and check because their objects, invariants, tools, and evidence standards differ.

  • Method

    EULER coordinates competing direct, adjacent-domain, and distant-domain routes, retaining bridges only when stress tests, executable operation gain, and checked source-side return pass.

  • Results

    Bridge-specific stress tests reduced incorrect source-side conclusions from 9 to 3, and bridge material plus target-native operations produced a positive interaction of 4.2 resolved tasks.

  • Takeaways & Limitations

    Domain distance did not determine success; executable operation gain, structural stress-test passage, and complete return evidence were the useful bridge conditions.

  • Takeaways & Limitations

    Results apply most directly to recent open problems with a strong combinatorial component, and contamination screening cannot eliminate undetected paraphrases or implicit memorization.

Abstract

from arXiv · show

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.

1 Introduction

EULER treats cross-community transfer as a bridge-search problem, requiring new target-side operations and checked return to the fixed source statement. It evaluates competing routes with early stress tests on 120 recent conjectures, finding strong safety and interaction effects while leaving the overall resolution difference uncertain.

  • System motivation: EULER searches direct, adjacent-domain, and distant-domain routes competitively around a fixed source problem.Bridges connect source objects to target-native operations and retain budget only after validation.
  • Illustrative trace: The Zhao conjecture was refuted after corrected indexed bit-mask encoding, exhaustive subset enumeration, and human substitution of the witness into the source statement.The first encoding failed a round-trip test because it merged equal-valued occurrences.
  • Bridge criteria: A bridge must supply an operation unavailable in the source representation and return target evidence through a checked implication.Verified resolution requires coverage of every obligation needed for a proof or counterexample.
  • Evaluation motivation: 120 recent conjectures were frozen and screened for answer cues to reduce the risk that apparent discovery reflects recall or recombination.The benchmark prioritizes timestamped problems because famous conjectures may have extensive exposure in training data.
  • Bridge criteria: Six bridge-specific stress tests reject errors in direction, assumptions, boundary cases, round trips, tool gain, or return before expensive search.These checks determine whether a route stops, receives refinement, or enters deeper target search.
  • Results: Bridge-specific stress tests reduced incorrect returns from 9 to 3, while the overall resolution difference remained uncertain at this sample size.The reported task-level paired difference was 4.2 percentage points with a 95% interval of [−0.1, 8.4].

2 System overview

EULER separates resource control, open-ended execution, verification, and persistent mathematical state while keeping their interfaces narrow. Versioned records and independent checking distinguish target progress from source-level mathematical resolution.

  • Four layers: EULER assigns control, execution, verification, and mathematical-state layers distinct responsibilities in each run.The state layer stores task and claim graphs, while verification records connect computational artifacts to mathematical dependencies.
  • Control: The control layer allocates budgets from recorded stress-test results, passed checks, return costs, and remaining resources.Narrative assessment alone cannot update route budgets.
  • Execution: Execution agents generate routes, retrieve mechanisms, invoke deterministic tools, and construct candidate Lean proofs.The layer combines heterogeneous models with enumeration, computer algebra, SAT/SMT, field-specific checkers, and Lean.
  • Verification: Verification audits bridge direction, assumptions, preserved structure, round trips, and source-side coverage using independent replay.A route proposer cannot certify its own output.
  • Mathematical state: The task graph records actions and budgets, whereas the claim graph records exact statements, evidence, dependencies, and versions.Completing target search does not automatically create a claim usable by later reasoning.
  • Versioning: Evidence is keyed by problem, route, bridge, and claim versions, preventing earlier bridge evidence from automatically supporting a revision.Model replacement does not change the mathematical dependency structure.

3 Method: bridge search and stress testing

EULER treats direct, adjacent-domain, and distant-domain approaches as competing routes, retaining bridges only when they add executable operations and support a checked return to the source statement. Ordered stress tests reject invalid bridges before costly target search.

  • A bridge records source and target objects, forward and return maps, changed assumptions, target operations, and return obligations.
  • Bridge validity depends on the admissible implication direction, because a one-way map may refute a source statement without proving it.
  • Domain distance scores changes in object type, theory, invariant, correspondence length, and expert community; totals 0–4 are adjacent and 6–10 are distant.
  • Routes compete under a utility score while preserving direct, adjacent, and distant representatives, so distance itself does not earn reward.
  • A BridgeOpportunity summarizes a target mechanism, expected operation, preserved quantities, losses, rejection test, return outline, and cost before becoming a mathematical claim.
  • The six stress tests proceed from low-cost structural checks to target-side tool and return checks, using bounded refinement or paired probes when inconclusive.

4 State and verification

EULER separates execution planning from mathematical state, linking them through candidates, artifacts, and verification records. Multiple evidence axes and centralized admission preserve scope, provenance, compositional closure, and reversible recovery.

  • Task and claim graphs: The task graph records execution order, dependencies, budgets, failures, and recovery, whereas completion of an artifact does not establish mathematical support.
  • Task and claim graphs: The claim graph stores versioned source and target statements, bridges, lemmas, counterexamples, and evidence-linked mathematical relations.
  • Task and claim graphs: Candidates, artifacts, and verification records connect execution to claims, but the root source statement changes only after the return chain is complete.
  • Evidence and composition: Four evidence axes separately track machine checks, semantic correspondence, independent review, and compositional coverage; quality and novelty do not alter truth status.
  • Evidence and composition: Separate axes expose scope mismatches, unchecked novelty, and local lemmas that fail to compose despite individual correctness.
  • Evidence and composition: Composition requires coverage, interface compatibility, invariant compatibility, well-foundedness, joint choice, and closure across the parent’s parameter range.
  • Admission and verification: A centralized updater admits claims only after contract-specific checks of versions, scope, dependencies, evidence, semantic correspondence, and closure.
  • Admission and verification: Independent replay records checker identity, environment, inputs, scope, axioms, artifacts, and results, while semantic review compares quantifiers, definitions, assumptions, cases, and direction.

5 Dataset and mathematical outcomes

The evaluation uses a frozen, contamination-screened set of 120 conjectures sampled through a recent JCTA-author frame. EULER produced verified proofs and refutations alongside scoped partial results, while several cases exposed source-return limits.

  • Dataset construction: The sampling frame uses recent JCTA publication as an external activity indicator, but the resulting cohort is not representative of all combinatorics or mathematics.
  • Dataset construction: Eligibility screening recovered fixed scopes from public conjectures, questions, and problems, merged duplicate content, and remained blind to system outcomes.
  • Aggregate outcomes: 638 papers yielded 286 candidate conjectures, 214 deduplicated statements, and 120 fixed tasks; outcomes were 10 proofs, 3 refutations, 27 conditional results, 18 local theorems, 59 unresolved tasks, and 3 incorrect conclusions.
  • Aggregate outcomes: The 13 verified resolutions used Lean kernel coverage for 3 tasks, independent deterministic replay for 3, and separate checks by two mathematicians for 7.
  • Aggregate outcomes: Across five reasoning seeds, the full system resolved 12, 12, 13, 13, and 14 tasks, with a mean of 12.8.
  • Stratified outcomes: The executable-refutation stratum resolved 5 tasks, the structural-transfer stratum 4, and the language-formalization and sparse-bridge strata 2 each.
  • Stratified outcomes: Structural-transfer errors came from returning a valid target theorem beyond its proof scope, while a sparse-bridge error reversed map direction.
  • Mathematical traces: A group-theoretic construction produced nine indexed zero-sum subsequences of fixed length 10, contradicting the conjectured equality through s≤9(G) ≥13 > 12 = D(G) + 1.

6 Evaluation and ablations

Across 120 fixed source tasks, EULER evaluates competing bridge routes, stress tests, executable-operation gains, budget feedback, heterogeneous agents, persistent state, and verified source-level outcomes. The experiments support stress-test filtering and bridge–operation interaction, while route-resolution and cost advantages remain uncertain.

  • 6.1 Evaluation protocol: 120 fixed source tasks were evaluated at the source-task level, with verified resolution as the primary endpoint and blinded dual review plus adjudication.Intervals used 10,000 source-task bootstrap resamples, and paired binary endpoints used two-sided exact tests.
  • 6.2.1 Route pools: The full-system resolution difference versus distant-domain retrieval was 4.2 percentage points with a 95% interval of [−0.1, 8.4], so the interval crossed zero.The full system resolved seven tasks in this comparison, as did distant-domain retrieval; the paired exact-test result was p = 0.125.
  • 6.2.2 Stress-test strength and order: 13 verified resolutions and 3 incorrect conclusions followed bridge-specific testing, versus 12 verified resolutions and 9 incorrect conclusions without those tests.The wider route pool produced more useful candidates but also more opportunities for wrong returns.
  • 6.2.3 Bridge material and target-native operations: 4.2 resolved tasks, or 3.5 percentage points, measured the interaction between bridge material and target-native operations.Without bridge material, the target-native operation added 0.6 verified resolutions; with bridge material, it added 4.8, and the interval was [1.0, 7.4] resolved tasks.
  • 6.2.5 Budget reallocation: Round-by-round budget reallocation produced two more resolutions than one-shot allocation and reduced rejected-bridge budget by seven percentage points.Released budget moved to surviving distant-domain bridges with target-operation gain, while unproductive adjacent-domain bridges received no further allocation.
  • 6.3 Multi-agent execution: Heterogeneous multi-agent execution averaged 12.8 resolutions at the same total budget, compared with 11.1 for homogeneous execution and 9.6 for a single agent.Ten of the 13 verified resolutions involved at least one cross-model handoff.
  • 6.4 Persistent state: Persistent task and claim graphs reduced repeated target runs to 4, stale returns to 0, recovery time to 34 minutes, and revoked unrelated claims to 5.The comparison used no persistent state, a task graph only, and both task and claim graphs.

7 Limitations

The evaluation is most directly applicable to recent open problems with strong combinatorial structure and inexpensive verification, while broader mathematical coverage, retrieval, novelty assessment, review, and deployment remain constrained.

  • Scope: The 120-task results apply most directly to recent open problems with strong combinatorial structure, finite counterexamples, and executable verification procedures.Analysis, geometry, and highly abstract algebra often lack inexpensive early rejection tests and require longer dual-domain expert review.
  • Measurement: The adjacent-versus-distant classification requires expert judgment and must be recalibrated for new mathematical areas.Annotators disagreed most often when a standard equivalence also introduced a new tool; score-5 gray-zone routes were excluded from the primary binary comparison.
  • Retrieval: Bridge retrieval favors communities with accessible literature, tool catalogs, and established verification procedures.Mechanisms outside the catalog still require an expert proposal before entering the candidate pool.
  • Evaluation: The contamination screen reduces identified exposure but cannot prove that proprietary training corpora contain no related material.Undetected paraphrases or implicit memorization may remain, and natural-language proof novelty requires active literature review.
  • Review: Verified resolutions remain subject to later specialist revision of standard lemmas, claimed equivalences, or parameter boundaries in long proofs.Per-task artifacts and dependency graphs restrict any revision to conclusions depending on the affected step.
  • Deployment: Deployment remains more complex than for a single mathematical agent because the implementation spans several services and formalization environments.Some environments and tools still require manual integration, despite measured recovery and replay costs.
  • Cost: At present cost, EULER is best suited to long-running problems where false conclusions are expensive and checked bridges can be reused.The upper cost confidence bound exceeds the noninferiority margin; combined cost also depends on expert-rate and review-allocation assumptions.

8 Conclusion

EULER concludes that successful cross-domain search depends on operational gain, stress-tested mappings, and complete source return rather than domain distance alone. Its linked task and claim records preserve reusable artifacts and support controlled route revision, while broader coverage and bridge reuse are the next priorities.

  • Conclusion: Across 120 recent open problems, EULER produced 10 proofs, 3 counterexamples, 27 conditional results, and 18 local theorems.Domain distance did not determine whether a route succeeded.
  • Conclusion: Bridge-specific stress tests reduced incorrect source-side conclusions from 9 to 3, while operation-set experiments found an interaction of 4.2 resolved tasks.The interaction equals 3.5 percentage points.
  • System design: Separate task and claim graphs preserve rejected-bridge counterexamples, local theorems, and dependency-limited effects of version changes.The task graph tracks pending work, while the claim graph records mathematical dependencies.
  • Future work: Future evaluation should broaden analysis, geometry, and algebra coverage while developing early rejection tests and reusing checked mappings and source-return templates.Reuse is proposed as the direct way to reduce the current 36-minute bridge-construction cost per task.
  • Bridge model: A bridge becomes a first-class object containing mappings, target mechanisms, expected operations, preservation information, source-return templates, tests, certificates, and budget.Route lineage connects revisions to bridge families and identifies which proof-critical component changed.
  • Route control: Route identity changes only with a structural change in the object map, target mechanism, or proof-critical source-return relation.Longer explanations or repeated retrieval remain the same route, whereas a changed map or source-return direction creates a new branch.

E Reproducibility bundle specification

The reproducibility bundle organizes each source task and run into fixed statements, route and verification records, artifacts, costs, events, and review entry points. It supports endpoint reconstruction, independent object checks, cost recomputation, and final claim-graph replay under controlled evidence and release tiers.

  • Bundle organization: Each task directory contains the fixed statement, source, contamination cutoff, and license metadata, while each run directory stores configuration, lineage, tests, artifacts, verification, decisions, costs, and events.A manifest maps every aggregate table cell to its corresponding per-task records.
  • Review entry points: The bundle’s review entry points check evidence scope, reconstruct primary and error endpoints, recompute costs and sensitivity analyses, and replay the final claim graph from an empty state.These checks are listed as independent review actions.
  • Release tiers: Seven verified resolutions belong to the complete release tier containing all listed layers.Witness-based and delayed-release tiers retain different subsets of artifacts while using the same outcome definitions.
  • Distance annotation: Distance scores classify routes as adjacent at 0–4, distant at 6–10, and gray-zone at 5, with gray-zone routes excluded from the primary binary comparison.Two annotators score five dimensions without seeing target results.
  • Stress tests: The six stress tests record bridge versions, preservation relations, methods, result codes, witnesses, scope, cost, obligations, and reopening conditions.PASS, FAIL, and UNKNOWN distinguish covered scope, concrete failure evidence, and the smallest next task.
  • Formalization: Formalization bridges apply the same template to natural-language and Lean statements, including quantifier maps, axioms, compilation environments, and semantic correspondence.The Lean kernel checks only the target operation, so semantic correspondence remains an explicit field.

H Capability matrix for experimental conditions

The capability matrix fixes comparable route conditions, eligibility rules, and task strata for direct, adjacent-domain, and distant-domain experiments. It also freezes the author frame and source-task contract before search, preserving task-level comparability across conditions.

  • Experimental conditions: The route-pool conditions specify capabilities and source-return rules for the experimental route classes.All six stress-test conditions share per-task limits on tokens, tool slots, target documents, cost, and expert minutes.
  • Controls: The full system and distant-domain retrieval share the same target-mechanism catalog and minimum eligibility screen.Distant-domain random selection and retrieval therefore differ in selection within a common eligible catalog.
  • Dataset frame: The author-eligibility window is the fixed closed 24-month interval ending at the frozen harvest cutoff Th.The window does not move with the paper’s publication or reading date.
  • Dataset frame: JCTA supplies an external author frame spanning finite and discrete structures across several combinatorial subfields.The frame targets active researchers at a recognized specialist level rather than ranking individuals or defining all combinatorics.
  • Dataset construction: Dataset construction enumerates eligible JCTA research articles, builds and disambiguates the author frame, collects public papers, extracts conjectures, deduplicates contracts, and samples four strata.The design samples 30 tasks from each of the four structural strata after eligibility screening without model attempts.
  • Task contract: Every source task fixes the statement, retrieval cutoff, evidence types, budget, boundaries, and source-side decision criteria before execution.Execution failures remain in the eligible denominator and do not trigger replacement.

I.1 Contamination audit and replacement rule

The audit separates overlap alerts from substantive contamination and freezes replacement decisions before execution. Evidence and verification procedures preserve scope, reproducibility, and independence across mathematical and computational checks.

  • Contamination audit: Only overlap containing a proof idea, counterexample, answer-bearing theorem, or query cue triggers replacement or blocking.Curators make this decision without seeing system outcomes, before execution is frozen.
  • Contamination audit: The protocol uses recency and date truncation to reduce exposure risk but does not certify that undetected contamination is absent.Restoration checks estimate the direction and size of detected contamination in the dataset.
  • Verification: Counterexamples require a generating route, independent recomputation, and source-side checking of statement version, quantifiers, scope, and violated conclusion.All three stages must agree before the evidence package is accepted.
  • Verification: Independent verification requires a second implementation, deterministic procedure, manual check, or formalization of the critical step; repetition alone is insufficient.Compact certificates such as counterexample coordinates or subset lists are preferred.
  • Verification: Finite computation supports only the statement scope it enumerates unless a separate theoretical step extends the result beyond that range.Root conclusions cite reproducible witnesses or a fixed statistical protocol for randomized exploration.

K Persistent-state experiment

The persistent-state experiment examines system behavior after three recoveries and two version changes, using a preregistered dependency reference to compare expected and observed claim effects.

  • K Persistent-state experiment: After three recoveries and two version changes, the experiment compares system output against a preregistered reference dependency table.The first recovery restarts only execution; later changes modify one bridge assumption and upgrade one target theorem.
  • K Persistent-state experiment: Unrelated withdrawals count claims rechecked despite not depending on the changed object.

L.1 Zhao counterexample certificate

The certificate constructs a length-12 sequence whose nonempty zero-sum subsequences all have length 10, yielding a source-side contradiction verified by exhaustive enumeration. The surrounding sparse-row theorem is limited to sparse rows, leaving dense AJT(5) open.

  • Source-side setup: D(G) = D∗(G) = 11 for the rank-four group used in the counterexample.The group has exponent 4 and satisfies every hypothesis of Zhao’s conjecture.
  • Certificate construction: The construction encodes selected multiplicities i, j, k and indicators α, β, γ, with Q = α + β + γ and selected length i+j+k+Q.The kernel analysis reduces nonempty zero-sum selections to the coefficient vector (2, 2, 2, 2).
  • Certificate construction: Every nonempty zero-sum subsequence of the length-12 sequence S has length 10, so S has none of length at most 9.There are nine indexed zero-sum subsequences, obtained by omitting one of p, q, r and choosing two copies from the corresponding repeated block.
  • AJT(5) sparse-row theorem: The sparse-row theorem covers every affine offset and dimension, while dense rows remain outside its scope and the general AJT(5) problem remains open.The proof counts solutions componentwise using row-support multigraphs and permutation-matrix bounds.

P Full Gao candidate-proof manuscript

The reproduced Gao manuscript presents a candidate proof of the Gao constant for generalized dihedral groups with an abelian odd-prime-group kernel. Its audit status remains provisional pending independent review and completion of a top-level Lean obligation.

  • Reproducibility: The 13 reproduced pages are delivered from a specified GitHub pull request, commit, companion LaTeX source, and build records.The snapshot was delivered through the paper-first arXiv rewrite branch.
  • Audit status: The reproduction is an audit surface, not a correctness certificate, and remains a complete natural-language candidate proof pending independent line-by-line review.Source-derived theorem instances and the top-level Lean obligation also require verification or completion.
  • Manuscript scope: The manuscript concerns generalized dihedral groups Dih(A) = A ⋊−1 C2 for nontrivial finite abelian p-groups with p odd.Its subject is the Gao constant for these groups.
  • Proof strategy: The upper-bound proof divides sequences by reflection count and combines weighted zero-sum results, a plus-minus Davenport bound, structural subgroup forcing, and simultaneous induction.The lower bound uses the known small Davenport constant of Dih(A).

1 Introduction

The paper determines the Gao constant of generalized dihedral groups with finite abelian p-group kernels for odd primes, proving equality with the group order plus the small Davenport constant. Its upper-bound proof combines rotation/reflection case analysis, weighted zero-sum arguments, and strict subgroup descent.

  • Bounds: The lower bound follows from E(G) ≥ |G| + d(G), while an explicit product-one-free construction illustrates the obstruction.The paper also records the equivalent bound E(G) ≥ 2Q + D(A) in the generalized dihedral setting.
  • Main result: E(Dih(A)) = |Dih(A)| + d(Dih(A)) for finite abelian p-groups A and odd primes p.Using d(Dih(A)) = D(A), this yields the exact value in terms of the kernel’s Davenport constant.
  • Main result: The theorem extends the cyclic-kernel formula to all invariant-factor decompositions of finite abelian p-groups with p odd.Earlier upper bounds did not determine the exact value for noncyclic kernels.
  • Proof strategy: The upper bound analyzes sequences by reflection count: few reflections use prescribed-length zero sums, many use plus-minus sums, and intermediate cases reduce to proper subgroups.The three regimes are handled by Propositions 4.1–4.3.
  • Scope: The proof relies on Olson’s Davenport-constant formula and a plus-minus argument over a field of odd characteristic, excluding mixed-prime kernels and 2-groups.These exclusions define the paper’s stated scope.
  • Proof strategy: Subgroup descent proves the required properties for every proper subgroup and supplies the induction needed to resolve the intermediate reflection range.The final proof applies descent after the intermediate-range reduction produces a nonzero proper subgroup K < A.
Loading 2609.00032v1…