Euler: Towards Human-Centered Multi-Agent Mathematical Discovery
Organizations: Shanghai Jiao Tong University · Ningbo Key Laboratory of Spatial Intelligence and Digital Derivative, Ningbo Institute of Digital Twin, Eastern Institute of Technology, Zhejiang, China · Institute of Automation, Chinese Academy of Sciences · Zhongguancun Academy, Beijing, China
Abstract
Mathematical research drives scientific discovery, and recent advances in AI for mathematics have shown that language-model agents can solve challenging problems and develop substantial mathematical proofs. Yet much of today's AI-for-mathematics work centers on obtaining a final answer. This emphasis leaves the exploration behind a result difficult for researchers to understand, while long-running investigations face fragmented context and the risk of unsupported claims propagating across reasoning steps. We present Euler, a human-centered mathematical research system built around a shared, structured representation of the research process. Euler organizes mathematical statements, assumptions, proof dependencies, alternative approaches, failed attempts, and verification evidence into connected research graphs. This representation allows researchers to trace how results are developed and supplies agents with persistent, task-relevant knowledge for planning, collaboration, and verification across sessions. Researchers can also select a graph node linked to a saved team state, revisit the agents' earlier reasoning, and explore alternative directions through continued interaction. We illustrate Euler's capabilities through three mathematical research case studies and describe the implemented system and its software validation.
Figures & tables
| Capability | Danus [ 2 ] | Euler (Ours) |
|---|---|---|
| Verified result memory | ✓ Fact Graph | ✓ Fact Graph + evidence links |
| Open research state | ✗ Not explicit | ✓ Goals, routes, blockers |
| State-guided context | ✗ Not documented | ✓ Scope-aware dependency retrieval |
| Human proof inspection | ✗ Dashboard / reports | ✓ Proof reader + graph views |
| Branchable continuation | ✗ No public team-state recovery | ✓ Checkpoints + native session forks |
| Agent coverage | ✗ Codex-centered team | ✓ Multi-provider adapters |
| Result | Recorded support | Frontier effect |
|---|---|---|
| Accepted claim | Matching statement, scope, required evidence | Discharge an obligation and update its dependents |
| Validated reduction | Checked closing argument with dependencies | Register a supported route and expose remaining premises |
| Checked counterexample | Witness with an aligned target and scope | Refute the affected local claim or route |
| Verified obstruction | Concrete checker or proof artifact | Refine the blocker and route options |
| New proposal | Source, author, target, and intended mechanism | Add an exploratory route or task |
| Execution outcome | Bound lease, context, and execution receipts | Update runtime status and resource accounting |
| Layer | Source modules | Main responsibility |
|---|---|---|
| Mathematical memory | core , gateway , verify | Shared findings, Fact Graph, admission and revocation |
| Research control | control | Contracts, obligations, frontier, scheduling, context, evidence, final audit |
| Agent execution | execution , providers , strategy | Worker rounds, provider adapters, consultation and execution receipts |
| Team recovery | workspace | Native sessions, messages, Git milestones and branch isolation |
| Research workbench | observability | Proof reading, graph navigation, live state, human requests, team conversations |
| Research outputs | write_paper , human_summary | Source-grounded manuscript and progress-report workflows |
| Case | Documented mathematical result | Research-state focus |
|---|---|---|
| Nikoghosyan | Hamiltonicity for finite, 1-tough, -free simple graphs on at least three vertices | Prerequisite closure and exact theorem assumptions |
| Lewis–Overton | Two nonterminating BFGS executions with distinct sharp trial-normalized rates for | Source conventions, paired constructions, and parameter scope |
| Jankiewicz–Norin–Wise | A 33-vertex witness for the four-connected legal-system obstruction question | Candidate exclusions, strategy changes, and hereditary subgraph conditions |
| Component | Validation coverage | Observed CI outcome |
|---|---|---|
| Offline Python suite | Research state, scheduler, verification adapters, recovery, API, and evaluation utilities | 1,352 pass; 2 skip (both Python versions) |
| Native team protocols | Provider session doubles and filesystem isolation on Linux/macOS | 56 pass (Linux); 53 pass, 3 skip (macOS) |
| Packaged dashboard | Wheel installation, six views, source graph, i18n, small-screen layout | Browser job passed |
| Mathematical examples | Manuscripts, formal repositories, historical graph snapshots | Companion artifacts; see Section 7 |