Euler: Towards Human-Centered Multi-Agent Mathematical Discovery

The distinction between the open Research Graph $\mathcal{R}_t$ (obligations, routes, blockers) and the verified Fact Graph $\mathcal{G}_t$ is a strong conceptual choice, and the context-compilation equations $C_t(a) = \operatorname{Compile}(\mathcal{P}, a, \mathcal{F}_t, D_t(a), H_t(a))$ with explicit size bounds are carefully formulated. The software engineering is commendable: the repository is open-source with detailed schemas, an append-only SQLite event store, and extensive CI outcomes reported as 1,352 passing tests and two skips on both Python 3.10 and 3.13.

The three mathematical case studies are not live autonomous runs in the current system; as the authors note, they are "source-bound records of investigations conducted across earlier workflow revisions." This makes them illustrative visualizations rather than reproducible evidence of Euler’s discovery capabilities. The paper also claims novel features over Danus based on published documentation gaps, but does not experimentally isolate the contribution of, for example, branchable continuation or state-guided context. A more serious reliability concern is that LLM proof review is treated as an admissible evidence tier alongside Lean kernel checks within the same predicate $\operatorname{Admissible}(e,o)$, even though the authors acknowledge that "LLM proof review has a different assurance level from Lean-kernel verification."

The architectural comparison to Danus is largely consistent with the source: Danus provides progress reports and a paper-writing system for human interaction, but does not publicly expose an explicit open-research frontier with graph-based proof inspection or recoverable team states. Euler fairly positions itself among concurrent systems (Rethlas/Archon, MMAT, Albilich, Magenta, LEAP) by emphasizing human inspectability and persistent context. Nevertheless, the absence of any quantitative baseline—no measured success rate, cost, or human effort comparison—means the evidence supports architectural novelty but not practical superiority.

The code is publicly versioned (commit ea505c7) and backed by 1,352 passing unit tests plus deterministic fixtures for protocol behavior. However, reproducing the actual mathematical case studies is blocked because they are historical snapshots rather than scripted autonomous runs, and because agent prompts, model hyperparameters, and frontier-scheduling policies are not specified. Native team recovery also requires excluded provider credentials, so a third party can verify software state transitions but not the research trajectories reported.