EULER

EULER is a local-first research workbench for auditable mathematical investigation. It combines a typed research kernel, durable evidence storage, verification gates, orchestration, command-line tools, HTTP APIs, SDKs, and a browser interface.

This repository is the public demonstration and reference implementation of EULER. It may lag behind the system used in active research.

Current public versions:

• EULER Workbench: 1.3.0
• Research Kernel (RK): 0.3.0
• Python: 3.12 or later
• Node.js: 22 or later

What EULER provides

Area	Capabilities
Research records	Versioned problems, claims, routes, evidence, reviews, revocations, and reports
Mathematical authority	Explicit separation between candidate output, machine verification, semantic review, peer review, quality review, and closure
Evidence	Content-addressed artifact storage, digests, provenance, upload contracts, and reproducible exports
Orchestration	Durable work items, route planning, budgets, resumable execution, adapters, and verifier planning
Verification	Lean replay support, deterministic certificate checks, independent review records, and dependency-aware invalidation
Research tools	Literature connectors, material extraction, local computation, LaTeX compilation, and configurable model or prover adapters
Interfaces	rkctl, a versioned HTTP service, Python and TypeScript SDKs, and the EULER browser workbench
Operations	SQLite persistence, schema migrations, backup and restore, health checks, local or remote execution, and release packaging

The central authority path is:

EULER Workbench / SDK / CLI
            |
            v
ResearchProduct service
            |
            v
ResearchKernel
            |
            v
SQLite + content-addressed storage

User interfaces and adapters cannot promote mathematical claims by writing directly to storage. State changes pass through the product service and the kernel's validation rules.

Repository layout

apps/euler/          Current EULER React workbench
src/rk/              Research kernel and product service
sdk/python/          Python SDK
sdk/typescript/      TypeScript SDK and EULER client
docs/spec/           Machine-readable public contracts
migrations/          Database migrations
schema_fragments/    Product schema fragments
packaging/           Build, service, and deployment helpers
scripts/             Administration and verification utilities
tests/               Unit, contract, migration, recovery, and end-to-end tests

Install the Python package

Clone the repository and create a virtual environment:

git clone https://github.com/randomcat4/EULER.git
cd EULER
python -m venv .venv

Activate it on Linux or macOS:

source .venv/bin/activate

Or on Windows PowerShell:

.venv\Scripts\Activate.ps1

Install the kernel:

python -m pip install --upgrade pip
python -m pip install -e .
rkctl --version

Optional symbolic-mathematics dependencies are available through:

python -m pip install -e ".[math-tools]"

This adds SymPy and Z3. Lean, Mathlib, search services, and model endpoints are optional external components and must be configured separately.

Start a command-line research project

Initialize a data directory. Credentials are read from the named environment variable and should never be written to the repository:

rkctl init ./rk-data \
  --model <model-name> \
  --endpoint https://provider.example/v1/chat/completions \
  --key-env MODEL_API_KEY

Create and complete a problem template, then submit it:

rkctl --config ./rk-data/config.json prepare ./problem.json
rkctl --config ./rk-data/config.json submit-run ./problem.json

Use the run identifier returned by the submission command:

rkctl --config ./rk-data/config.json status <run-id>
rkctl --config ./rk-data/config.json continue <run-id>
rkctl --config ./rk-data/config.json pause <run-id>
rkctl --config ./rk-data/config.json resume <run-id>
rkctl --config ./rk-data/config.json report <run-id> --format html --output report.html

Run rkctl --help or rkctl <command> --help for the complete command set. The CLI includes English aliases while preserving its native Chinese interface.

Configure Lean and Mathlib

To enable authoritative Lean replay, point an initialized service directory at a real Lean toolchain and Mathlib checkout:

rkctl configure-math ./rk-data \
  --Mathlib路径 /path/to/mathlib4 \
  --Lean工具链 /path/to/lean

On the native Chinese CLI, the exact option names are also shown by:

rkctl configure-math --help

Missing optional proof or retrieval components are reported as unavailable; they are not converted into successful verification results.

Start the product service

Bootstrap a local product data root:

python scripts/rkproductbootstrap.py \
  --data-root ./product-data \
  --deployment-id local-rk \
  --organization-id local-org

The bootstrap command writes an initial credential file inside the data root. Keep it private and outside version control. Select the managed review identity and secret from that file, expose the secret only to the service process, and start the backend:

export RK_REVIEW_HMAC_SECRET="<review-secret>"
python -m rk.http.production_runtime \
  --data-root ./product-data \
  --deployment-id local-rk \
  --organization-id local-org \
  --review-key-id managed-peer-review \
  --reviewer-identity-id "<reviewer-identity-id>" \
  --host 127.0.0.1 \
  --port 8080

Use the equivalent PowerShell environment-variable syntax on Windows:

$env:RK_REVIEW_HMAC_SECRET = "<review-secret>"

The service exposes health and versioned /v1 routes on the configured interface.

Start the EULER workbench

In a second terminal:

cd apps/euler
npm ci
npm run sdk:build
EULER_API_ORIGIN=http://127.0.0.1:8080 npm run dev

Windows PowerShell:

Set-Location apps/euler
npm ci
npm run sdk:build
$env:EULER_API_ORIGIN = "http://127.0.0.1:8080"
npm run dev

Open http://127.0.0.1:4173. The development server proxies /v1 and /healthz to EULER_API_ORIGIN.

The workbench includes:

• persistent research threads and branches;
• conversation, scratchpad, and work-graph surfaces;
• artifact upload and inspection;
• authority, review, dossier, and recovery views;
• configurable primary instances and execution backends;
• activity streaming, search, command palette, and settings;
• read-only and managed-session access modes.

Build and verify

Install development dependencies and run the Python checks:

python -m pip install -e ".[dev]"
python -m pytest
python -m ruff check .
python -m mypy src/rk

Verify the current workbench:

npm --prefix apps/euler ci
npm --prefix apps/euler run verify

Build the TypeScript SDK independently:

npm --prefix sdk/typescript ci
npm --prefix sdk/typescript run build

Build the contract bundle:

python packaging/build_release.py --output dist/rk-product-service-contracts.zip

Configuration and security

• Start from config.example.toml; keep deployment-specific values in an untracked local copy.
• Supply model keys, review secrets, SSH credentials, and capability keys through the environment or external secret files.
• Do not commit product data roots, SQLite files, content-addressed artifacts, generated credentials, or private research material.
• Bind development services to loopback unless an authenticated reverse proxy and transport security are configured.
• Treat model output and tool success as candidate evidence until the applicable verification gate accepts them.

License

EULER is released under the MIT License.