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
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
Figure 1: The Euler research loop. A fixed mathematical target and persistent research records determine an active frontier. Agents receive contexts for selected obligations, produce arguments or computational evidence, and return checked outcomes to the shared state. The same underlying objects are presented to the human researcher through the workbench.
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
Table 1: Published architecture features of Danus and Euler.
Figure 2: An illustrative AND/OR frontier. Two proposed routes compete to establish T . Evidence closes A and excludes the route requiring B ; a checked reduction of C creates obligations D and E . The active fringe moves as supported claims and route relations change.
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
Table 2: Evidence-mediated changes to the research state.
Figure 3: Selected dependency chain from the Lewis–Overton research graph. The displayed route runs from rate semantics and scale-free update through the five-trial and four-trial constructions to distinct sharp rates and the final initial-state-dependence result.
Figure 4: Milestone-restoration dialog in the Euclid onboarding exercise. The panel identifies the selected proof object, the saved checkpoint, the recovered branch contents, and the availability of native team conversations. The researcher may attach an optional follow-up question before opening the restored workspace.
Figure 6: Review of the derived BFGS question, assumptions, and execution allowance before dispatch.
Figure 7: Source-linked lifecycle of a focused BFGS investigation, from the researcher’s question to its recorded outcome.
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
Table 3: Principal software components in the current Euler repository.
Case
Documented mathematical result
Research-state focus
Nikoghosyan
Hamiltonicity for finite, 1-tough, (P4∪P1) -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 9/5<u<13/6
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
Table 4: Mathematical scope and representation questions in the three case studies.
Figure 8: Selected proof modules leading to Nikoghosyan’s Hamiltonicity theorem. The overview exposes the principal prerequisite dependencies.
Figure 9: Nikoghosyan’s original target and its recorded acceptance basis in the proof reader.
Figure 10: Proof structure for the Lewis–Overton investigation. The five-trial and four-trial execution families establish distinct sharp rates, which are compared to derive initialization dependence. Each module links to its exact conditions and evidence.
Figure 11: The Jankiewicz–Norin–Wise case. The overview identifies the proof obligations of the constructed host, while the research-route records preserve the candidate-search history and the later successful construction mechanism.
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
State Key Laboratory of Mathematical Sciences, Academy of Mathematics and Systems Science, CAS · School of Mathematical Sciences, University of Chinese Academy of Sciences · School of Advanced Interdisciplinary Sciences, University of Chinese Academy of Sciences