Governance substrate for verifiable learning: deterministic replay, dual attestation, fail-closed claims.
Live Demo arXiv License: Apache-2.0
MathLedger Demo Pipeline
========================
┌─────────┐ ┌─────────┐ ┌────────────┐ ┌───────────┐
│ Input │ ──▶ │ Run │ ──▶ │ Artifacts │ ──▶ │ verify.py │
│ (seed) │ │ (demo) │ │ (output/) │ │ │
└─────────┘ └─────────┘ └────────────┘ └───────────┘
│
▼
┌────────────┐
│ PASS / FAIL│
└────────────┘
Determinism guarantee: same seed → byte-identical artifacts → same hash
# Prerequisites: Python 3.11+, uv package manager uv run python scripts/run_dropin_demo.py --seed 42 --output demo_output/ cd demo_output && python verify.py
Expected output:
[PASS] Composite root verified: H_t == SHA256(R_t || U_t)
No database or external services required. The demo runs fully offline.
| You want to... | Start here |
|---|---|
| Run the demo (2 min) | scripts/run_dropin_demo.py |
| Understand what you're looking at | docs/HOW_THE_DEMO_EXPLAINS_ITSELF.md |
| Audit artifacts independently | docs/pilot/AUDIT_WALKTHROUGH.md |
| See the sealed FOL specification | docs/FOL_FIN_EQ_PHASE3_CLOSURE.md |
| Browse all documentation | docs/README.md |
| Try the live hosted demo | mathledger.ai/demo |
| Read the paper | docs/PAPERS/mathledger_arxiv_preprint.pdf |
After running the demo, demo_output/ contains:
demo_output/
├── verify.py # Self-contained verifier (run this)
├── evidence_pack.json # Complete audit artifact
├── manifest.json # Execution metadata
├── u_t.txt # UI Merkle root
├── r_t.txt # Reasoning Merkle root
├── h_t.txt # Composite root: SHA256(R_t || U_t)
└── replay_instructions.md # Third-party reproduction steps
The verify.py script recomputes all hashes locally with no external calls. If replay produces different hashes, the pack is invalid.
- Governance substrate: separation of exploration from authority at the data model level
- Deterministic attestation: same inputs → same hashes, every time
- Fail-closed claims: ABSTAINED is a first-class outcome, not a missing value
- Auditable by design: evidence packs enable independent replay verification
- A capability demonstration (the demo does very little on purpose)
- A production system (governance substrate only)
- A safety claim (we claim legibility, not alignment)
- A convergence guarantee (learning dynamics are Phase II)
Running the boundary demo at mathledger.ai/demo produces:
1. ADV (Advisory) "2 + 2 = 4" → ABSTAINED Excluded from authority stream
2. PA (Attested) "2 + 2 = 4" → ABSTAINED Authority-bearing but no validator
3. MV (Validated) "2 + 2 = 4" → VERIFIED Arithmetic validator confirmed
4. MV (False) "3 * 3 = 8" → REFUTED Arithmetic validator disproved
Conclusion: Same claim text, different trust class → different outcome.
Same trust class, different truth → VERIFIED vs REFUTED.
This demonstrates authority routing, not proof generation.
Verify first-order logic formulas with equality over finite domains:
python -m scripts.run_fol_fin_eq_demo --domain z2 --output demo_z2 python demo_z2/verify.py
Expected output:
PASS: All certificates verified
Golden manifest SHA256: 096ee79e4e20c94fffbc2ec9964dde98f8058cba47a887031085e0800d6d2113
See docs/FOL_FIN_EQ_PHASE3_CLOSURE.md for the sealed specification.
For external reviewers conducting artifact verification:
| Document | Purpose |
|---|---|
docs/pilot/AUDIT_WALKTHROUGH.md |
Complete audit procedure |
docs/pilot/PILOT_NON_CLAIMS.md |
Binding non-claims |
docs/pilot/PILOT_EVALUATION_CHECKLIST.md |
22-item PASS/FAIL checklist |
docs/FOR_AUDITORS.md |
Cold-start auditor guide |
This audit verifies artifact integrity and determinism only; it makes no correctness, safety, or compliance claims.
MathLedger: A Verifiable Learning Substrate with Ledger-Attested Feedback
@misc{mathledger2025, title={MathLedger: A Verifiable Learning Substrate with Ledger-Attested Feedback}, author={MathLedger Contributors}, year={2025}, eprint={2601.00816}, archivePrefix={arXiv}, primaryClass={cs.AI}, url={https://arxiv.org/abs/2601.00816} }
Full documentation index: docs/README.md
| Category | Key Documents |
|---|---|
| Demo | HOW_THE_DEMO_EXPLAINS_ITSELF.md, V0_LOCK.md |
| Audit | FOR_AUDITORS.md, pilot/AUDIT_WALKTHROUGH.md |
| Specs | FOL_FIN_EQ_PHASE3_CLOSURE.md, invariants_status.md |
| Ops | DEPLOY_BY_TAG_DOCTRINE.md, VERSION_NUMBER_DOCTRINE.md |
Apache-2.0