allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
Research-Stack/docs/math-first-tooling.md
Devin AI 87960676b4 Add math-first tooling: receipt schema, claims registry, pre-commit, CI, MCP 
Adds automated guardrails so mathematical rigor is enforced by tooling
instead of by convention. See docs/math-first-tooling.md for the full
contract.

Schemas + registry:
- shared-data/schemas/deepseek-review-receipt.schema.json
  Draft 2020-12 schema for the existing ollama_deepseek_review_receipt_v1
  and ollama_deepseek_review_continuation_receipt_v1 receipt formats. Pins
  sha256:<hex> hashes, non-negative token counts, repo-relative POSIX
  paths, and rejects additional fields.
- shared-data/schemas/claims-registry.schema.json
  Schema for claims.yaml. Requires review_receipts when status is
  verified-by-ai and a lean source when status is formally-proven.
- claims.yaml
  Initial registry entry: prime-gap-entropy-collapse (verified-by-ai)
  linked to the two existing receipts under
  shared-data/artifacts/deepseek_review/.

Validators (scripts/math-first/):
- validate_deepseek_receipts.py: validates tracked or passed receipts
  against the JSON Schema; shared by pre-commit and CI.
- test_validate_deepseek_receipts.py: positive + 7 negative fixtures
  asserting exit-code behaviour.
- validate_claims_registry.py: schema check + unique id check + on-disk
  existence check for every referenced repo-relative path.
- require_math_evidence.py: gate that requires a DeepSeek receipt, a
  Lean change, or a claims.yaml update alongside edits to math-track
  surfaces (Lean Semantics kernels, ArithmeticSpec docs, stack
  solidification receipts).

Pre-commit (.pre-commit-config.yaml):
- check-json, check-yaml, end-of-file-fixer, trim trailing whitespace,
  detect-private-key (scoped to math-first files only per AGENTS.md
  Do Not Sweep).
- Local hooks wiring all three math-first validators above.

CI (.github/workflows/math-check.yml):
- validate-schemas: compiles every schema, runs both validators, runs
  the validator self-tests, then re-invokes the canonical Ollama
  emitter in --verify-only mode against every tracked receipt to
  re-check answer_sha256 against the answer-file bytes on disk.
- require-evidence: enforces the math-track evidence rule at PR scope.
- pre-commit: runs all pre-commit hooks against the PR diff so the
  contract holds even for contributors who skip installing hooks
  locally.

MCP (.mcp.json):
- filesystem, sympy, wolfram-alpha, lean, deepseek-review entries
  pointing at off-the-shelf upstream servers and at the canonical
  ollama_deepseek_review_emitter.py. Secrets stay in the runtime env
  (WOLFRAM_ALPHA_APPID, OLLAMA_API_KEY) and are never embedded.

Docs (docs/math-first-tooling.md):
- Philosophy, surfaces, schema reference, registry workflow, hook
  catalogue, CI catalogue, MCP catalogue, end-to-end verify command.

shared-data/schemas/*.schema.json and claims.yaml live under paths the
top-level .gitignore would normally exclude; they are force-added via
git add -f the same way existing promoted receipts under
shared-data/artifacts/deepseek_review/ are tracked (per AGENTS.md).

Co-Authored-By: Allaun Silverfox <bigdataiscoming+9i37y6j2@protonmail.com>
2026-05-12 04:25:52 +00:00

253 lines
12 KiB
Markdown
Raw Blame History

# 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`](../shared-data/schemas/deepseek-review-receipt.schema.json) |
| Claim registry schema | [`shared-data/schemas/claims-registry.schema.json`](../shared-data/schemas/claims-registry.schema.json) |
| Claim registry | [`claims.yaml`](../claims.yaml) |
| Receipt validator | [`scripts/math-first/validate_deepseek_receipts.py`](../scripts/math-first/validate_deepseek_receipts.py) |
| Registry validator | [`scripts/math-first/validate_claims_registry.py`](../scripts/math-first/validate_claims_registry.py) |
| Evidence gate | [`scripts/math-first/require_math_evidence.py`](../scripts/math-first/require_math_evidence.py) |
| Pre-commit config | [`.pre-commit-config.yaml`](../.pre-commit-config.yaml) |
| CI workflow | [`.github/workflows/math-check.yml`](../.github/workflows/math-check.yml) |
| MCP server registry | [`.mcp.json`](../.mcp.json) |
Read [`AGENTS.md`](../AGENTS.md) and
[`6-Documentation/wiki/DeepSeek-Review-Process.md`](../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, Lean, and DeepSeek bridges
they need to discharge proof obligations — and nothing else.
## 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`](../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`](../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
```bash
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:
```bash
python3 scripts/math-first/validate_deepseek_receipts.py \
shared-data/artifacts/deepseek_review/<topic>_<model>_<ts>.receipt.json
```
The validator has its own self-tests:
```bash
python3 scripts/math-first/test_validate_deepseek_receipts.py
```
## Mathematical Claim Registry
[`claims.yaml`](../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. |
```bash
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`](../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`. 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`).
### Install
```bash
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`](../.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`](../.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` | Wraps `ollama_deepseek_review_emitter.py` so an assistant can request a fresh review and receive a receipt path back. | `OLLAMA_API_KEY`. |
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
```bash
# 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/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.
Reference in a new issue View git blame Copy permalink