getting-started

Getting started

Install the monorepo toolchain, run the local engineering gate, and exercise offline replay / the Agent API. MathEvidence remains experimental — read ../STATUS.md and ../security/KNOWN_TRUST_GAPS.md before relying on any capability.

Prerequisites

• Lean toolchain matching the committed lean-toolchain
• Python 3 with the repo requirements files (requirements.txt / requirements-dev.txt, or the project’s uv/pyproject.toml workflow)
• just

Optional:

• SymPy (open reference backend; used by several conformance paths)
• wolframscript when exercising live Mathematica adapters (MATHEVIDENCE_WOLFRAMSCRIPT)

Clone and check

git clone https://github.com/fraware/MathEvidence.git
cd MathEvidence
just check

just check runs the local engineering gate: Lean build, audits, schema/registry validation, Python tests, conformance, replay, and related harnesses.

Windows: kernel-replay rsp (required)

On Windows with Lean v4.14, bare lake build mathevidence-kernel-replay often fails to link (CreateProcess error 206 / command line too long). The required local path is the response-file helper:

python scripts/link_exe_via_rsp.py mathevidence-kernel-replay
just exe-smoke

just exe-smoke / scripts/smoke_exe.py attempt rsp automatically and, if linking still fails, degrade with replay_dependency_missing (never fake Certified). Linux CI (.github/workflows/lean.yml) remains the authoritative linked-exe attestation (--self-test + --self-test-analytic). Details: ../audits/2026-07-26-real-vision/KERNEL_REPLAY_PLATFORM.md.

Focused trust subset:

pytest tests/forensic -q

CI honesty: workflow definitions live under .github/workflows/. A green local just check is not promotion evidence and is not an attested immutable CI green on a release commit.

First offline replay

Committed Evidence Bundle trees under evidence/ use schema v0.2 (.cjson) for full bundles. Prefer replaying through the documented CLI / mathevidence-verify-bundle (temporary alias mathevidence-replay), or through the Agent API below.

For rational equality, the verifier emits operational native_checked / checker_accepted only — not theorem Certified / kernel_replay. Do not treat backend status codes as theorems. Replay must recheck committed evidence without trusting the solver.

Theorem-level Certification Records require exact candidate binding and a registry crEligible capability — see ../STATUS.md and ../HANDOFF.md.

Agent API (local)

python -m agent.api.server --host 127.0.0.1 --port 8787

Health: GET http://127.0.0.1:8787/v1/health

Public open / inspect / replay accept opaque bundleId values from the content-addressed store only — raw filesystem paths are rejected. See ../../agent/README.md.

Formal vs analytic calculus

Registry id	Scope
algebra.formal_rational_calculus	Formal rational-expression calculus only
analysis.analytic_calculus	Analytic whitelist (Deriv / DerivWithin / Antideriv / ODE)

Formal calculus does not establish Mathlib HasDerivAt / analytic ODE theorems. Exact analytic ODE currently requires empty domain obligations and at most one initial condition; multi-IC / obligation-bearing ODE fail closed.

Next reading

Doc	Why
../STATUS.md	Preview claims, CR eligibility, non-claims
../HANDOFF.md	Exact-certification engineering runbook
../security/KNOWN_TRUST_GAPS.md	Trust gaps
../products/README.md	Product surface map
../architecture/README.md	Architecture notes
../../CONTRIBUTING.md	Contribution rules