MathTrace is an AI-powered mathematical problem-solving workflow and formal verification runtime. It combines autonomous multi-agent mathematical reasoning with rigorous, tamper-evident audit trails, native execution with optional Linux sandboxes, and interactive Lean 4 proof checking.
MathTrace structures mathematical inquiry into an immutable, ledger-backed process—ensuring that every theorem, proof obligation, computational step, and counterexample is tracked, verified, and preserved with complete provenance.
- Immutable Transactional Ledger: All mathematical claims, assumptions, inferences, and campaign events are recorded in an append-only SQLite store with cryptographic SHA-256 state digests.
- Scoped Evaluation & Cycle Detection: Inferences are evaluated within strict local scopes using conservative antitone bounds and selected witness forests (
scoped-selected-forest-v3), preventing circular logic and premature global assertions. - Nonparty Adjudication & Challenge Resolution: Formal objections, refutations, and counterarguments are adjudicated independently by nonparty review protocols, preventing silent substitution of historical audit witnesses.
- Formal Proof Verification: Proof code is verified using a pinned official Lean 4 toolchain and checked-target primitive-context replay. Native execution is the default; Linux Bubblewrap is optional. Standalone fresh checks retain
leanchecker --fresh. - Adaptive Frontier Coordination: Campaigns dynamically project active problem frontiers, track multi-step obligation lineage, and manage committed work intents with crash-resilient, idempotent recovery.
- Advisory Learning Layer: Heuristics, proof tactics, and empirical research patterns are curated against verified event lineage to advise reasoning agents without contaminating deductive proof graphs.
- Native Multi-Agent Roles: Specialist agent roles (strategists, provers, falsifiers, adjudicators, and formalizers) operate under tool-free, isolated boundaries with attributable terminal transcript recording.
MathTrace/
├── mathtrace/ # Core Python runtime, CLI, and Lean semantic inspector
├── tests/ # Comprehensive regression test suite
├── tools/ # Developer setup, package validation, and native installers
├── docs/ # Operational guides, workspace map, and architectural decisions
│ ├── README.md # Detailed repository navigation guide
│ ├── architecture/ # Authoritative architectural records and review dispositions
│ ├── coordination.md # Adaptive frontier and obligation tracking
│ ├── evaluation.md # Scoped support, refutations, and witness forests
│ ├── evidence.md # Computational receipts and formal checking boundaries
│ ├── execution.md # Durable intent, sandbox isolation, and recovery
│ ├── native-capture.md # Terminal observation and host attribution limits
│ ├── completion.md # Criteria fulfillment and stopping criteria
│ └── learning.md # Advisory extraction, curation, and target admission
├── openspec/ # OpenSpec specifications, changes, and configuration
├── coding-harnesses/ # Agent harness definitions for supported environments
└── work/ # Local validation runs, toolchains, and recovery archives (not committed)
- Python: Version 3.11 or newer.
- Operating System: Windows, Linux or macOS. Native execution requires no WSL or container.
- Optional Execution Sandbox: Select
execution_mode: "bubblewrap"explicitly to use Linux Bubblewrap andlibseccomp, including the existing Windows/Ubuntu WSL transport. - Interactive Theorem Prover: Pinned Lean v4.30.0 toolchain (provisioned by the
install_leanruntime operation).
Install into your project with Node 22+ and Python 3.11+:
npx mathtrace@latestSelect your installed coding harness from the numbered menu. MathTrace installs its runtime and integration inside the current project. See installation for prerequisites, supported hosts, optional execution isolation, and safe updates.
Install MathTrace in development mode or as a standalone wheel:
# Clone or navigate to the repository
cd MathTrace
# Install Python package in editable mode
pip install -e .Only when choosing optional Bubblewrap execution, provision its Linux or WSL environment:
python tools/setup_execution.pyThe MathTrace CLI provides a unified control surface for campaign administration:
# Display CLI identity and available commands
python -m mathtrace identity
python -m mathtrace --help
# Initialize a new mathematical campaign database
python -m mathtrace init --db .math/state.sqlite
# Check campaign database health and state digest
python -m mathtrace health --db .math/state.sqlite
# Export a state snapshot
python -m mathtrace snapshot --db .math/state.sqliteCreate a JSON contract definition (e.g., contract.json):
{
"statement": "For every positive real x, x squared is positive.",
"definitions": [],
"completion": "An exact proof or a domain-valid counterexample."
}Register the contract into the campaign ledger:
python -m mathtrace contract --db .math/state.sqlite --input contract.jsonThe CLI returns an immutable contract identifier used for downstream claim registration, inference submission, and candidate auditing.
MathTrace equips AI agents and human researchers with specialized skills:
/mathtrace-help: Interactive discovery guide explaining workflows, specialist roles, and research phases./math-intake: Formalizes problem statements, definitions, and completion contracts./math-research: Explores lemmas, candidate proof branches, and computational experiments./math-formalize: Translates informal arguments into verified Lean 4 declarations./math-audit: Runs multi-dimensional audits on frozen solution candidates./math-release: Finalizes audited solutions and issues release receipts.
To update or synchronize the local agent environment in .agents/:
python tools/install_native.pyMathTrace includes a comprehensive test suite covering database transactions, cycle detection, witness forest memoization, Lean checking integration, and host capture isolation:
# Run full deterministic test suite
pytest tests
# Build and validate isolated package wheel
python tools/validate_package.py
# Validate OpenSpec specifications and changes
openspec validate --allProject maintenance and feature development are governed strictly through OpenSpec. System requirements and verified capability behaviors are documented under:
openspec/specs/
Before proposing changes, review the coding agent instructions in AGENTS.md and the operational guides in docs/.
Copyright © 2026 Velor-dev. Public project author/developer: Velor-dev.
MathTrace is proprietary and source-available, with free personal, academic, and commercial use under LICENSE. The license permits installation and necessary project-local/internal operational copies, while reserving general modification and redistribution rights. The separate OpenSpec development-skill notice is included in LICENSE.
When publishing your own project, exclude installed MathTrace software assets (including its runtime, skills, agents, and copied guides) and direct users to install the official distribution. Your original research, proofs, results, and project files are not restricted merely because you used MathTrace. Do not remove your own shared instruction files; exclude only copied MathTrace material from public redistribution. These permissions do not override third-party terms.
The official npm package is mathtrace. Publication requires an assembled,
integrity-verified payload; package publication does not create a GitHub release.