Research-Stack/docs/math-first-tooling.md

Math-First Tooling

This document codifies the "math first" contract for the Research Stack: every mathematical claim that ships from this repository must carry machine-checkable evidence — a Lean proof, a DeepSeek review receipt with SHA-256 integrity, or both — and the development environment must make it harder to bypass that contract than to honour it.

It is the human-readable companion to:

Artifact	Path
Receipt schema	shared-data/schemas/deepseek-review-receipt.schema.json
Claim registry schema	shared-data/schemas/claims-registry.schema.json
Claim registry	claims.yaml
Receipt validator	scripts/math-first/validate_deepseek_receipts.py
Registry validator	scripts/math-first/validate_claims_registry.py
Evidence gate	scripts/math-first/require_math_evidence.py
Pre-commit config	.pre-commit-config.yaml
CI workflow	.github/workflows/math-check.yml
MCP server registry	.mcp.json

Read AGENTS.md and 6-Documentation/wiki/DeepSeek-Review-Process.md first — this document layers tooling on top of those contracts and does not restate them.

Philosophy

1. Lean is the source of truth. Anything that can be stated as a Lean theorem or kernel obligation should live under 0-Core-Formalism/lean/Semantics/. Other evidence (DeepSeek reviews, SymPy/Wolfram cross-checks, hardware receipts) is a witness, not a proof.
2. Every claim has a status. The states are conjecture → verified-by-ai → formally-proven → published. Movement only ever travels in that direction, and every transition is accompanied by a change to claims.yaml.
3. Receipts pin model output to disk. DeepSeek answers and their *.receipt.json siblings carry prompt_sha256 and answer_sha256 so a review can be re-validated without re-running the model.
4. CI enforces the contract. Anything humans are expected to remember is re-checked by a workflow that fails the PR if the contract is broken.
5. AI assistants get tool access, not trust. The .mcp.json registry gives Claude / Devin / Codex the Wolfram, SymPy, and Lean bridges they need to discharge proof obligations — and nothing else. DeepSeek review remains available through the canonical CLI emitter until a real MCP wrapper exists.

Repository Layout (math-first surfaces)

0-Core-Formalism/lean/Semantics/      # Lean source of truth (lakefile.toml)
shared-data/schemas/                   # JSON Schemas for every receipt format
shared-data/artifacts/deepseek_review/ # Promoted DeepSeek review receipts
shared-data/data/stack_solidification/ # Stack receipts (math-track)
6-Documentation/docs/distilled/        # Distilled math specs (math-track)
scripts/math-first/                    # Validators + evidence gate
claims.yaml                            # Single source of truth for claims
.pre-commit-config.yaml                # Local guardrail
.github/workflows/math-check.yml       # CI guardrail
.mcp.json                              # AI-assistant tool registry

Receipt Schema (ollama_deepseek_review_receipt_v1)

The schema at shared-data/schemas/deepseek-review-receipt.schema.json formalises the contract that the canonical emitter 5-Applications/tools-scripts/llm/ollama_deepseek_review_emitter.py already writes. It validates two receipt flavours:

• Primary review (ollama_deepseek_review_receipt_v1) — requires schema, created_at, model, endpoint, prompt_sha256, answer_sha256, usage.{prompt_tokens,completion_tokens,total_tokens}, context_files (non-empty), and answer_path.
• Continuation review (ollama_deepseek_review_continuation_receipt_v1) — replaces context_files with previous_answer_path and optionally reports the message_keys returned by the continuation endpoint.

Both flavours pin SHA-256 hashes as the literal string sha256:<64 hex>, require token counts to be non-negative integers, and require paths to be repo-relative POSIX strings ending in .md for answer paths. Additional fields are rejected so receipts stay shaped exactly as the emitter writes them.

Re-validate locally

uv run --python 3.11 \
  --with "jsonschema>=4.21" --with "rfc3339-validator" \
  python3 scripts/math-first/validate_deepseek_receipts.py

To validate a single receipt:

python3 scripts/math-first/validate_deepseek_receipts.py \
  shared-data/artifacts/deepseek_review/<topic>_<model>_<ts>.receipt.json

The receipt validator and the evidence gate both have self-tests:

python3 scripts/math-first/test_validate_deepseek_receipts.py
python3 scripts/math-first/test_require_math_evidence.py

The require_math_evidence self-test includes a regression for the pre-commit files-filter bug: it builds a throwaway repo, stages a math-track file plus a receipt, then invokes the script with --staged to confirm both files are visible end-to-end.

Mathematical Claim Registry

claims.yaml is the single source of truth for the rigor level of every tracked mathematical claim. The schema accepts these fields:

Field	Required	Notes
id	yes	Stable kebab-case slug.
title	yes	One-line natural-language statement of the claim.
status	yes	conjecture | verified-by-ai | formally-proven | published.
lean	conditional	Required when status == formally-proven. Repo-relative Lean source path.
review_receipts	conditional	Required when status == verified-by-ai. Repo-relative *.receipt.json paths.
sources	no	Supporting docs, scripts, or external citations.
notes	no	Free-form context.

uv run --python 3.11 \
  --with "jsonschema>=4.21" --with "PyYAML" \
  python3 scripts/math-first/validate_claims_registry.py

The validator enforces the JSON Schema, asserts every id is unique, and asserts every repo-relative path referenced from lean, review_receipts, or sources exists on disk.

Pre-Commit Hooks

.pre-commit-config.yaml wires four guardrails:

• pre-commit-hooks — check-json, check-yaml, EOF / trailing whitespace scoped to math-first files only (see AGENTS.md "Do Not Sweep"), and detect-private-key.
• deepseek-receipt-schema — runs the receipt validator on every staged *.receipt.json under shared-data/artifacts/deepseek_review/.
• claims-registry-schema — runs the registry validator whenever claims.yaml is staged.
• receipt-required-for-math-content — invokes scripts/math-first/require_math_evidence.py --staged. If a commit touches a math-track surface (0-Core-Formalism/lean/Semantics/, 6-Documentation/docs/distilled/, shared-data/data/stack_solidification/), the same commit must also touch a math-evidence surface (a DeepSeek receipt, a Lean kernel, or claims.yaml). The hook is configured with always_run: true and pass_filenames: false so the script reads the entire staged set via git diff --cached --name-only; pre-commit's per-hook files filter would otherwise strip evidence files from the argv before the script could see them.

Install

uv tool install pre-commit          # one-time, per machine
pre-commit install                  # one-time, per clone
pre-commit run --all-files          # smoke-test

CI Workflow

.github/workflows/math-check.yml runs on every PR and on pushes to main or distilled that touch a math-first surface. It has three jobs:

1. validate-schemas — compiles every schema under shared-data/schemas/, validates every tracked DeepSeek receipt, runs the validator's own self-tests, validates claims.yaml, and finally re-runs the canonical emitter in --verify-only mode against every receipt to re-check answer_sha256 against the answer file bytes on disk. This is the AGENTS.md contract for promoted Ollama/DeepSeek review receipts.
2. require-evidence — runs only on PRs and invokes scripts/math-first/require_math_evidence.py --from-git-diff origin/<base> to enforce the same evidence rule at PR scope that the pre-commit hook enforces at commit scope.
3. pre-commit — runs every pre-commit hook against the PR's range of changed files (pre-commit run --from-ref <base> --to-ref HEAD), so the guardrails are honoured even when a contributor has not installed the hooks locally.

The pre-existing wolfram-verification.yml workflow continues to police mathematical formulas inside Lean source for missing Wolfram Alpha verification comments; nothing here replaces it.

MCP Servers for AI-Assisted Math

.mcp.json declares the math-first tool surface that Claude Desktop, Devin, and other MCP-aware clients should advertise when working in this repo. Each server is intentionally gated on a runtime environment variable, so the config itself never carries secrets and contributors who have not provisioned a backend simply skip it.

Server	Purpose	Runtime requirement
filesystem	Read/write proof artifacts, Lean kernels, receipts.	npx, scope pinned to repo root.
sympy	Local SymPy bridge for symbolic verification of arithmetic claims.	uv tool run sympy-mcp (sympy-mcp upstream).
wolfram-alpha	Wolfram Alpha verification for the formulas policed by wolfram-verification.yml.	WOLFRAM_ALPHA_APPID.
lean	Lean 4 / Mathlib typecheck bridge against 0-Core-Formalism/lean/Semantics/lakefile.toml.	elan on PATH with leanprover/lean4:v4.30.0-rc2.
DeepSeek review	Use 5-Applications/tools-scripts/llm/ollama_deepseek_review_emitter.py directly; no MCP server is currently advertised for it.	OLLAMA_API_KEY for non-local endpoints.

To use these from Claude Desktop, point its claude_desktop_config.json at the repo root or copy the relevant entries verbatim. Secrets live in the shell/env, never in the config.

Workflow: adding a new claim

1. Land the natural-language claim in claims.yaml with status: conjecture.
2. Produce a DeepSeek review via the canonical emitter. Commit both the answer markdown and *.receipt.json; promote status to verified-by-ai in the same commit. The pre-commit require-evidence gate now finds a receipt alongside any math-track edit, and the schema validator confirms the receipt parses.
3. When a Lean proof lands under 0-Core-Formalism/lean/Semantics/, promote status to formally-proven and set lean: to the proof's source path.
4. On external publication, promote status to published and add the citation to sources:.

Workflow: editing a math-track file

The math-first surfaces are:

• 0-Core-Formalism/lean/Semantics/...
• 6-Documentation/docs/distilled/...
• shared-data/data/stack_solidification/...

Any commit touching one of these surfaces must, in the same commit, touch one of:

• shared-data/artifacts/deepseek_review/... (new receipt + answer file)
• 0-Core-Formalism/lean/Semantics/... (Lean change in the same commit counts as evidence — Lean is the source of truth)
• claims.yaml (registry update)

The pre-commit hook and CI both enforce this. To bypass intentionally — for example, a typo fix in a distilled doc with no semantic change — commit with git commit --no-verify and explain the bypass in the PR description; CI will still flag the PR and the maintainer can apply the math-first-exempt label (one-off override).

Verifying everything in one shot

# Schemas + receipts + claims + emitter --verify-only
uv run --python 3.11 \
  --with "jsonschema>=4.21" --with "rfc3339-validator" --with "PyYAML" \
  bash -c '
    python3 scripts/math-first/validate_deepseek_receipts.py \
      && python3 scripts/math-first/test_validate_deepseek_receipts.py \
      && python3 scripts/math-first/test_require_math_evidence.py \
      && python3 scripts/math-first/validate_claims_registry.py \
      && for r in shared-data/artifacts/deepseek_review/*.receipt.json; do \
           python3 5-Applications/tools-scripts/llm/ollama_deepseek_review_emitter.py --verify-only "$r"; \
         done
  '

If any of the above fails, the corresponding PR will not merge.