mdblueprint

mdblueprint is a Markdown-first blueprint system for mathematical knowledge bases that are meant to work with Lean. It keeps small Markdown files as the durable source of truth, then uses deterministic Python tools to validate the dependency graph, check mechanical Lean references, export machine-readable graph data, and publish a leanblueprint-style static site.

It does not use LaTeX, plasTeX, or leanblueprint as the source pipeline. The project borrows the useful presentation style of leanblueprint while keeping the source model simple enough for humans and AI agents to edit safely.

Agent Entry Points

This repository is designed so Codex, Claude Code, OpenCode, and other coding agents can work on it at the same time without sharing hidden state.

Human overview: this README.md.
Agent operating rules: AGENTS.md.
Claude Code compatibility shim: CLAUDE.md, which points back to AGENTS.md.
Detailed agent role contracts: docs/agent-contracts.md.
Skills and how to install/use them: docs/skills.md.
GitHub Actions publishing setup: docs/github-integration.md.

When in doubt, an agent should read AGENTS.md first, then the specific docs for the files it plans to edit.

What This Tool Owns

mdblueprint separates mathematical source, deterministic build products, and AI assistance:

Durable source:
  docs/knowledge/nodes/**/*.md      admitted mathematical nodes
  docs/knowledge/staged/**/*.md     candidate nodes under review
  docs/knowledge/reviews/**/*.md    verifier and referee reports
  docs/knowledge/requests/**/*.md   requests for missing or revised nodes

Deterministic Python output:
  graph.json
  graph_topics.json
  subgraphs/topics/*.json
  node_payloads/*.json
  topic pages
  keyword pages
  node pages
  dep_graph_document.html / graph.html

AI-assisted output:
  staged candidate nodes
  review reports
  Lean proposals
  alignment reports
  requests for missing nodes

Python tools, not LLMs, generate the final graph, reverse dependencies, HTML pages, and static-site index pages.

Install

Use Python 3.10 or newer.

uv sync --extra dev

If you are not using uv, install the package in editable mode and install the development dependencies from pyproject.toml.

pip install -e '.[dev]'

Quickstart For Humans

Validate the example knowledge base:

uv run python -m tools.knowledge.check docs/knowledge

Publish the static site to a temporary directory:

uv run python -m tools.knowledge.publish docs/knowledge /tmp/mdblueprint-site

Preview the generated site locally:

python -m http.server 8001 --directory /tmp/mdblueprint-site

Then open:

http://127.0.0.1:8001/index.html

Run the full test suite:

uv run --extra dev python -m pytest -q

Development Commands

Run commands from the repository root.

# Install development dependencies
uv sync --extra dev

# Full Python test suite
uv run --extra dev python -m pytest -q

# Focused graph and publisher tests
uv run --extra dev python -m pytest tests/test_export.py tests/test_publish.py tests/test_graph_navigation_docs.py -q

# Structural check for the example knowledge base
uv run python -m tools.knowledge.check docs/knowledge

# Structural + semantic lint (see docs/lint.md for the rule reference)
uv run mdblueprint-lint docs/knowledge

# Publish a local preview outside the source tree
uv run python -m tools.knowledge.publish docs/knowledge /tmp/mdblueprint-site

# Browser render check for generated math and graph pages
uv run --extra browser python -m tools.knowledge.render_check /tmp/mdblueprint-site

# Real EconCSLib integration gate
uv run --extra browser python -m tools.knowledge.econcslib_gate --render-mode smoke

For first-time browser checks, install Chromium once:

uv run --extra browser playwright install chromium

GitHub Sync Contract

main is the shared integration branch for mdblueprint. Multiple agents should use short-lived branches or worktrees for active work, then merge or fast-forward only after verification.

# See local state before starting or handing off
git status --short --branch

# Sync main without rewriting history
git fetch origin
git pull --ff-only origin main

# Push completed verified work
git push origin main

Rules for concurrent agents:

Treat GitHub issues as the coordination queue. Claim the issue or state the file set you are editing before making broad changes.
Use one branch or worktree per agent task when work can overlap.
Do not rewrite another agent's files, force-push shared branches, or clean untracked files that you did not create.
Keep generated artifacts out of commits unless the issue explicitly asks for a committed fixture.
Close issues only after tests or the real-library gate relevant to that issue have passed.

Command Reference

Call the tools as Python modules from the repository root.

# Structural checks for nodes, staged candidates, dependencies, cycles,
# math syntax, and configured Lean repository references
uv run python -m tools.knowledge.check docs/knowledge

# Or run one-off Lean prechecks before repository config exists
uv run python -m tools.knowledge.check docs/knowledge --lean-root path/to/lean/project

# Generate graph.json and the static HTML site
uv run python -m tools.knowledge.publish docs/knowledge /tmp/mdblueprint-site

# Generate with an explicit project config
uv run python -m tools.knowledge.publish docs/knowledge /tmp/mdblueprint-site --config path/to/mdblueprint.yml

# Strict browser render verification for published math
uv run --extra browser python -m tools.knowledge.render_check /tmp/mdblueprint-site

# Real-library integration gate for check, publish, topic graph artifacts, and bounded render QA
uv run --extra browser python -m tools.knowledge.econcslib_gate --render-mode smoke

# Index Lean declarations from a Lean project
uv run python -m tools.knowledge.lean_index path/to/lean/project

# Build bounded candidates for connecting one Markdown node to existing Lean
uv run python -m tools.knowledge.lean_link_candidates docs/knowledge --node-id <node-id>

# Validate or apply a mechanical Lean link proposal
uv run python -m tools.knowledge.lean_linking docs/knowledge --proposal proposal.yml
uv run python -m tools.knowledge.lean_linking docs/knowledge --proposal proposal.yml --apply

# Build or validate a bounded Markdown-Lean semantic alignment report
uv run python -m tools.knowledge.lean_alignment docs/knowledge --node-id <node-id> --declaration <Lean.Declaration>
uv run python -m tools.knowledge.lean_alignment docs/knowledge --report alignment.yml

# Run the Python-orchestrated admission pipeline after review gates pass
uv run python -m tools.knowledge.admission_pipeline docs/knowledge/staged/example.md docs/knowledge

# Legacy direct admission helper
uv run python -m tools.knowledge.admit docs/knowledge/staged/example.md docs/knowledge

The publisher refuses to delete the knowledge source tree. For local previews, prefer publishing to /tmp/... or another build directory outside docs/knowledge.

Browser render verification uses Playwright. Before the first run, install the browser runtime:

uv run --extra browser playwright install chromium

The real-library gate uses the current mdblueprint checkout, clones EconCSLib main by default, runs check, publishes the site, verifies graph_topics.json graph_topics_hierarchy.json, and per-topic subgraphs/topics/*.json payloads, requires published Lean references to resolve to source URLs unless explicitly allowed, then render-checks a bounded smoke set of pages. It logs the source checkout, source ref, exact source commit, generated site directory, checked pages, and graph artifact locations.

Use a local EconCSLib checkout when testing pending knowledge-base changes:

uv run --extra browser python -m tools.knowledge.econcslib_gate \
  --repo-path /path/to/EconCSLib \
  --site-dir /tmp/mdblueprint-econcslib-gate \
  --render-mode smoke

Use --render-mode all before release when a change could affect broad browser rendering behavior.

Use --allow-unresolved-lean-refs only for an intentional transitional gate run where raw Lean declarations are acceptable. Normal gate runs fail when generated node payloads contain Lean declarations without resolved source_url fields.

EconCSLib Relationship

mdblueprint is the tooling repository. EconCSLib is the real Lean/knowledge-base consumer used as the integration target.

Changes to tools/knowledge/check.py, publish.py, export.py, templates, graph behavior, Lean link resolution, or node schema can change what EconCSLib publishes.
EconCSLib's workflow is expected to run mdblueprint from GitHub, currently from mdblueprint main unless the workflow pins another ref.
Pushing mdblueprint main can therefore affect the next EconCSLib blueprint build even if EconCSLib itself has no code change.
EconCSLib content changes live in the EconCSLib repository. mdblueprint should not carry domain-specific knowledge except small generic fixtures or documented integration references.
Before merging broad publisher, graph, schema, or Lean-link changes, run the local real-library gate against a current EconCSLib checkout when available:

uv run --extra browser python -m tools.knowledge.econcslib_gate \
  --repo-path /path/to/EconCSLib \
  --site-dir /tmp/mdblueprint-econcslib-gate \
  --render-mode smoke

Use --render-mode all for release-level checks or after changes to math rendering, navigation, graph JavaScript, or page templates.

Project Config

The generated site is named by the blueprint project, not by the publishing tool. Put the project-level site config at docs/knowledge/mdblueprint.yml:

site:
  title: Algebra Library Blueprint
  short_title: Algebra
math:
  macros:
    R: "\\mathbb{R}"
  delimiters:
    inline:
      - ["\\(", "\\)"]
      - ["$", "$"]
    display:
      - ["\\[", "\\]"]
      - ["$$", "$$"]
  throw_on_error: false
graph:
  max_visible_nodes: 120
  max_expand_nodes: 80
  proof_plans: selected-only
lean:
  default_repository: core
  repositories:
    - id: core
      title: Example Lean Library
      local_path: ../example-lean
      web_url: https://github.com/example/example-lean
      source_url_template: "{web_url}/blob/{revision}/{path}#L{line}"
      revision: auto

Project config contract:

site.title is the homepage H1 and the suffix in browser titles.
site.short_title is the sidebar logo when present.
If site.short_title is omitted, the sidebar logo uses site.title.
If no config exists, publishing still works and derives a deterministic neutral title from the knowledge root.
The CLI accepts --config path/to/mdblueprint.yml to use a config outside the knowledge root.
math.macros declares project macros once; use the macro name without the leading slash.
math.macros is for genuinely custom macros. KaTeX built-ins such as notin, ldots, ast, subseteq, and widetilde are accepted without project declarations, and declarations that would override known built-ins are not passed to KaTeX.
math.delimiters.inline and math.delimiters.display control the KaTeX auto-render delimiters.
Prefer \(...\) for inline math and \[...\] for display math in new nodes; dollar delimiters remain enabled by default for compatibility.
Markdown preservation and static math diagnostics are designed around the default delimiter family; use custom delimiter syntax only with browser render verification.
math.throw_on_error is passed to KaTeX as throwOnError; keep it false for browsing and use tools.knowledge.render_check for strict release checks.
graph.max_visible_nodes caps a rendered graph state; the default is 120.
graph.max_expand_nodes caps direct topic expansion; the default is 80.
graph.proof_plans controls proof-plan visibility in expanded topic views and must be hidden, selected-only, or all; the default is selected-only.
lean.repositories configures Lean Git repositories that nodes may reference.
lean.default_repository is optional; when present, nodes may omit lean.repository.
lean.repositories[*].local_path may be absolute or relative to the config file and must point at the Lean root used for module paths.
lean.repositories[*].revision may be a literal revision or auto; auto resolves to the Git HEAD commit in local_path.
lean.repositories[*].source_url_template uses {web_url}, {revision}, {path}, and {line} to build stable published declaration links.

Read docs/math-authoring.md for supported node math syntax, macro authoring, static diagnostics, and browser render QA. Read docs/lean-repositories.md for the full Lean repository linking workflow, diagnostics, and publishing contract.

Repository Structure

tools/knowledge/
  models.py          node, source, Lean, verification dataclasses
  parser.py          YAML frontmatter and Markdown body parser
  validator.py       schema validation for admitted and staged nodes
  graph.py           dependency DAG builder with cycle detection
  export.py          deterministic graph.json export
  check.py           structural checker CLI
  blueprint_view.py  leanblueprint-style presentation model and DOT export
  publish.py         static-site publisher
  lean_index.py      Lean declaration indexer
  lean_check.py      mechanical Lean reference prechecks
  admit.py           staged-to-admitted workflow
  templates/         generated-site HTML, CSS, and graph JS

docs/
  architecture.md
  github-integration.md
  lean-repositories.md
  math-authoring.md
  node-format.md
  topic-model.md
  agent-contracts.md
  publisher-and-dag.md
  reference-repos.md
  skills.md

docs/knowledge/
  mdblueprint.yml    project site title and short title
  nodes/             admitted Markdown nodes
  staged/            candidate Markdown nodes
  reviews/           verifier/referee reports
  requests/          proposed missing or revised nodes

Using Skills

The repo includes workflow skills under skills/ for humans and AI agents. They are the recommended entry points for recurring mdblueprint tasks.

Task	Skill
Extract theorems, definitions, examples, or proof ideas from a book, PDF, paper, TeX source, or notes	`mdblueprint-source-extraction`
Recover a proof, proof sketch, or hint for an existing theorem-like node from cited source spans	`mdblueprint-source-proof-recovery`
Create or edit a Markdown knowledge node by hand	`mdblueprint-node-author`
Review staged nodes before admission	`mdblueprint-node-review`
Generate Lean declarations or proof skeletons from admitted nodes	`mdblueprint-lean-generation`
Propose mechanical links from Markdown nodes to existing Lean declarations	`mdblueprint-lean-linking`
Check semantic alignment between Markdown and Lean	`mdblueprint-alignment-review`
Publish or inspect the generated site and dependency graph	`mdblueprint-publish`

If your assistant does not auto-discover repo-local skills, open the relevant skills/<name>/SKILL.md and follow it manually. See skills/README.md and docs/skills.md for Claude Code and Codex installation notes.

Proof repair is source-first: if a theorem-like node has source.spans, the Python workflow should try source proof recovery before bounded proof-fill. Proof-fill may use an explicit source hint supplied by the orchestrator, but it must not read source files directly.

The Node Model

Each mathematical object is one Markdown file with YAML frontmatter and a math-only body.

---
id: algebra.groups.group
title: Group
kind: definition
status: admitted
primary_topic: algebra.groups
topics:
  - algebra.groups
uses:
  - algebra.sets.binary_operation
tags:
  - algebra
  - group-theory
verification:
  definition: accepted
  proof: not_applicable
  alignment: pending
---

# Group

A group is a set $G$ with a binary operation $\cdot$, an identity element
$e$, and inverses, such that the operation is associative.

Important rules:

id is stable machine identity. It should not change just because topic views change.
primary_topic is the node's home topic and default owner.
topics lists the topic views where the node appears; one node may appear in several topic views.
title is the human-facing label used in the generated site.
kind controls theorem/definition styling and validation.
status records the workflow state.
uses lists logical dependencies by node id.
tags generate keyword pages.
The Markdown body should contain mathematics only, not process notes.

Read docs/node-format.md and docs/topic-model.md before creating or editing nodes.

Valid Kinds And Statuses

Supported node kinds:

concept
definition
lemma
proposition
theorem
example
proof-plan
external-theorem
task

proof-plan nodes are proof-route artifacts, not extra logical dependencies of their theorem. They must name the theorem-like target with target, may record route state with plan_status, and should put only proof-route dependencies in uses.

Supported statuses:

staged
needs_statement_review
needs_definition_review
needs_proof_review
admitted
formalized
proved
blocked
deprecated

Files under docs/knowledge/nodes/ should normally use admitted, formalized, or proved. Files under docs/knowledge/staged/ should use staged or a needs_* status.

Human Workflow

1. Add Or Edit An Admitted Node

Use this only when you are directly maintaining trusted source files.

Pick a stable id such as algebra.groups.group_homomorphism.
Check the nearest topics.md catalog and choose one primary_topic plus any additional topics memberships.
Put the file under docs/knowledge/nodes/<home-topic>/.
Write YAML frontmatter according to docs/node-format.md.
Keep the body mathematical. Write TeX according to docs/math-authoring.md, and do not add operational headings like "Status", "Implementation notes", or "Agent discussion".
Run:

uv run python -m tools.knowledge.check docs/knowledge
uv run python -m tools.knowledge.publish docs/knowledge /tmp/mdblueprint-site

2. Draft A Candidate Node

Use this for extracted, uncertain, or AI-proposed material.

Put the file under docs/knowledge/staged/.
Use status: staged or one of the needs_* statuses.
Include source spans when available.
Leave uses: [] if dependencies are unknown; do not invent dependencies.
Add review reports under docs/knowledge/reviews/.
When review gates pass, run:

uv run python -m tools.knowledge.admission_pipeline docs/knowledge/staged/example.md docs/knowledge

Admission checks staged schema, generality review, verification evidence, review evidence, and DAG validity before moving the node into docs/knowledge/nodes/. Definition and concept nodes require verification.definition: accepted. Lemma, proposition, theorem, and external-theorem nodes require verification.statement: accepted. If the body contains a proof block, admission also requires verification.proof: accepted. Ordinary admitted nodes may omit Lean metadata. Nodes with status formalized or proved must include lean.modules and lean.declarations.

3. Connect A Node To Lean

First configure the Lean repository in docs/knowledge/mdblueprint.yml. With a default repository, nodes can omit lean.repository; otherwise each node must name the repository id.

For first-time linking, use the bounded Python workflow instead of scanning the whole Lean repository by hand:

uv run python -m tools.knowledge.lean_link_candidates docs/knowledge --node-id <node-id>
uv run python -m tools.knowledge.lean_linking docs/knowledge --proposal proposal.yml

tools.knowledge.lean_link_candidates builds the candidate bundle, mdblueprint-lean-linking is the agent skill for choosing a mechanical link, and tools.knowledge.lean_linking validates the proposal and can apply only the lean: block with --apply. Semantic matching is separate: tools.knowledge.lean_alignment builds and validates bounded alignment reports. The linking step must not set verification.alignment, status: formalized, or status: proved.

Add a lean block when a node corresponds to Lean declarations:

lean:
  repository: core
  modules:
    - Example.Algebra.Groups
  declarations:
    - Example.Algebra.Group

Then run:

uv run python -m tools.knowledge.check docs/knowledge
uv run python -m tools.knowledge.publish docs/knowledge /tmp/mdblueprint-site

The Lean precheck is mechanical. It checks that modules and declarations exist, reports obvious sorry or admit markers, warns about dirty configured repositories, and reports ambiguous short declaration names. The publisher uses the same config to render source links in node pages and graph modals. It does not prove semantic alignment between Markdown and Lean.

Use --lean-root path/to/lean/project only for a one-off mechanical check before repository config exists. The publisher does not accept --lean-root; stable source links require lean.repositories config.

4. Publish The Website

uv run python -m tools.knowledge.publish docs/knowledge /tmp/mdblueprint-site

The generated site includes:

index.html: title-first topic outline
<topic>/index.html: topic pages
keywords/<tag>.html: tag-based keyword pages
<topic>/<node_id>.html: node pages with theorem/definition wrappers
dep_graph_document.html: topic-first Graphviz dependency graph with expandable topics and lazy node-detail modals
graph.html: compatibility alias for the dependency graph
graph.json: deterministic full machine graph export
graph_topics.json: topic overview graph used by the default graph page
graph_topics_hierarchy.json: topic parent/child hierarchy, aggregate counts, and child lists
subgraphs/topics/<topic>.json: per-topic expandable browsing subgraphs
node_payloads/<node>.json: lazy node-detail payloads used by graph modals

Graph navigation contract:

The default graph is topic-first so large knowledge bases open at a readable scale.
graph.json remains the full machine graph. Browser UI artifacts are derived browsing projections, not replacements for the machine export.
Topic ids are hierarchical. A node has one primary_topic home topic and may list several topics memberships for graph views.
Topic overview edges display dependency topic -> dependent topic.
Topic overview edges summarize ordinary mathematical dependencies. Proof-plan route edges stay out of the overview so candidate proof routes do not look like admitted topic dependencies.
Expanding a topic with child topics shows the next subtopic layer first. Expanding a leaf topic shows its internal node-level subgraph, plus dashed boundary topic nodes for external prerequisites and external users.
Breadcrumbs and explicit parent/root controls allow moving back up the topic hierarchy.
Node-level graph display uses dependency -> dependent, even though internal graph edges store dependent -> dependency.
Oversized topics use the configured graph limits and show links to the topic page and keyword pages instead of rendering an unreadable subgraph.
Graph node modals load node_payloads/<node>.json on demand.
Proof-plan nodes are proof routes attached by dotted has plan edges. The graph page visibility selector controls whether proof routes are hidden, selected only, or all shown.

Proof text is collapsed by default when the body contains a recognized proof marker:

*Proof.*
**Proof.**
Proof.
## Proof

The source file remains plain Markdown; proof folding is a presentation-layer feature.

AI And Agent Instructions

AI agents are welcome in this repository, but they must preserve the source/build boundary. The authoritative, detailed version is docs/agent-contracts.md. This README repeats the operational contract so an agent can start safely from this file alone.

Before changing anything, an agent should read:

Universal Agent Contract

Every agent must state or infer these fields before it writes files:

role: one of the contracts below;
inputs: exact files, source excerpts, Lean modules, or command outputs used;
outputs: exact files to write or patches to propose;
allowed write locations;
forbidden write locations;
decision vocabulary;
uncertainty behavior;
whether it may propose new nodes.

Every report-like output must start with machine-readable metadata:

agent: source-to-md | statement-verifier | proof-verifier | lean-generator | alignment-verifier | admission-referee
target:
  node_id: optional.node.id
  path: docs/knowledge/staged/example.md
decision: one value from this agent's decision vocabulary
created_at: "ISO-8601 timestamp"
inputs:
  - path/or/source/identifier
summary: one short sentence

The report body may explain reasoning in prose, but the decision field must remain machine-readable.

Global Permissions

create staged candidate nodes under docs/knowledge/staged/;
write review reports under docs/knowledge/reviews/;
write missing-node or revision requests under docs/knowledge/requests/;
propose Lean code or Lean patches;
edit admitted nodes only when the human explicitly asks for that exact edit;
run check, publish, and test commands.

Global Prohibitions

generate final graph.json by hand;
generate final HTML pages by hand;
invent final DAG edges or reverse-dependency lists;
write directly to docs/knowledge/nodes/ unless explicitly instructed;
mark a node admitted, formalized, or proved without the required evidence;
invent dependencies just to make the graph look connected;
put process notes, reviewer comments, or implementation plans in a node body;
silently broaden or weaken a mathematical statement;
treat Lean reference existence as semantic alignment.

Source-to-MD Contract

Purpose: convert PDFs, books, papers, TeX, or notes into staged Markdown candidate nodes.

Inputs:

source files or source excerpts;
source manifest or citation information;
target topic directory;
existing admitted and staged node index.

Allowed writes:

docs/knowledge/staged/**/*.md;
uncertainty or extraction notes under docs/knowledge/reviews/.

Forbidden writes:

docs/knowledge/nodes/**;
generated site files;
graph.json.

Decision vocabulary:

extracted
partial
uncertain
blocked

Rules:

search existing nodes before creating a candidate;
preserve source locators in source.artifacts and source.spans;
extract one reusable mathematical object per node;
use status: staged or a needs_* status;
do not invent dependencies beyond source evidence or existing node ids;
if the source statement is narrower than the likely reusable form, keep the source-local claim and ask the generality question in a report.

May propose new nodes: yes, but only as staged candidates with source locators.

Statement Or Definition Verifier Contract

Purpose: check that a staged or admitted statement/definition is mathematically correct, well-scoped, and general enough.

Inputs:

target node;
dependencies named by uses;
source spans when available;
project notation conventions when available.

Allowed writes:

review reports under docs/knowledge/reviews/;
optional revision or missing-dependency requests under docs/knowledge/requests/.

Forbidden writes:

admitted nodes;
generated site files;
final graph artifacts.

Decision vocabulary:

accepted
needs_revision
rejected

Rules:

verify assumptions, notation, dependency adequacy, and generality;
ask: "What is the most general useful form of this statement, and is the current form acceptable?";
do not silently rewrite admitted truth;
if a dependency is missing or a statement should be split, write a request rather than directly creating admitted content.

May propose new nodes: only through docs/knowledge/requests/.

Proof Verifier Contract

Purpose: check that proof text or a proof sketch proves the stated result.

Inputs:

node statement;
proof body or proof sketch;
dependencies named by uses;
relevant source spans or Lean declarations if available.

Allowed writes:

proof review reports under docs/knowledge/reviews/;
optional missing-lemma requests under docs/knowledge/requests/.

Forbidden writes:

admitted nodes;
generated graph or site files;
silent proof repairs without a report.

Decision vocabulary:

accepted
gap
critical

Rules:

identify exact gaps, hidden assumptions, circular reasoning, or misuse of prior nodes;
distinguish a local proof gap from a reusable missing lemma;
write a request for a reusable missing lemma instead of inserting it as admitted truth.

May propose new nodes: only through docs/knowledge/requests/.

MD-to-Lean Generator Contract

Purpose: generate Lean declarations, proof skeletons, or Lean patch proposals from admitted Markdown nodes.

Inputs:

admitted target node;
dependency nodes;
Lean declaration index;
existing Lean modules.

Allowed writes:

Lean patch proposals or generated Lean files when the human asks for code work;
docs/knowledge/requests/ for missing auxiliary mathematical nodes;
optional review notes explaining formalization choices.

Forbidden writes:

admitted Markdown nodes without a human request;
final graph or site files;
weakened Markdown statements without a review note.

Decision vocabulary:

generated
blocked_by_missing_node
blocked_by_missing_definition
blocked_by_lean_error
request_human

Rules:

generate Lean against admitted Markdown, not staged truth;
preserve the mathematical statement unless a report explicitly explains the mismatch;
propose auxiliary mathematical content only through docs/knowledge/requests/;
explain why a proposed auxiliary result should be a reusable node rather than a local Lean lemma.

May propose new nodes: yes, only through docs/knowledge/requests/.

External-Theorem Admission Contract

Purpose: admit a Markdown node for a theorem already proved in Lean, such as Mathlib or another Lean library result.

Inputs:

Lean module and declaration names;
Markdown statement;
source or Lean locator;
alignment review evidence.

Allowed writes:

admitted external-theorem node only when the workflow explicitly chooses the external-theorem direct-admission path;
alignment and admission reports under docs/knowledge/reviews/.

Forbidden writes:

generated graph or site files;
external-theorem nodes without Lean module and declaration references.

Decision vocabulary:

admit_external
needs_alignment
needs_statement_review
needs_human_decision
reject

Required node fields:

kind: external-theorem;
lean.modules;
lean.declarations;
verification.statement;
verification.alignment;
completed generality gate.

Required checks:

lean.modules and lean.declarations exist mechanically;
statement verifier decision is accepted;
alignment verifier decision is aligned or an explicitly acceptable lean_stronger;
no proof verifier is required when the proof already exists in Lean.

Forbidden behavior:

do not use external theorem admission to bypass statement review;
do not claim semantic alignment from declaration existence alone.

MD-Lean Alignment Verifier Contract

Purpose: decide whether a Lean declaration semantically matches a Markdown node.

Inputs:

Markdown node and dependencies;
Lean module and declaration references;
Lean declaration index or signatures;
mechanical precheck output.

Allowed writes:

alignment reports under docs/knowledge/reviews/.

Forbidden writes:

final status updates;
admitted node rewrites;
generated graph or site files.

Decision vocabulary:

aligned
lean_stronger
lean_weaker
lean_special_case
lean_extra_hypotheses
lean_missing_hypotheses
definition_mismatch
uncertain

Rules:

run or consume deterministic Lean reference prechecks first;
report extra hypotheses, missing hypotheses, weaker conclusions, stronger conclusions, specialization, or definition mismatch;
do not treat Python prechecks as semantic proof;
return an alignment report, not an automatic truth update.

May propose new nodes: no. It may request human review when a mismatch reveals missing mathematical content.

Admission Referee Contract

Purpose: decide whether a staged node and its evidence justify admission.

Inputs:

staged candidate node;
statement or definition verifier report;
proof verifier report when proof content exists;
generality gate answer;
deterministic Python check report.

Allowed writes:

admission report under docs/knowledge/reviews/;
controlled move into docs/knowledge/nodes/ only when the workflow explicitly approves admission.

Forbidden writes:

direct mathematical rewriting without a report;
admission when dependencies are missing or cyclic;
admission without a completed generality gate;
silent resolution of conflicting reports.

Decision vocabulary:

admit
needs_revision
needs_human_decision
reject

Rules:

if reports disagree, return needs_human_decision;
if checks fail, return needs_revision or reject;
when approved, use the admission workflow rather than manually copying files:

uv run python -m tools.knowledge.admit docs/knowledge/staged/example.md docs/knowledge

May propose new nodes: no.

Request File Contract

Any agent that wants new mathematical content but is not allowed to create an admitted node must write a request under docs/knowledge/requests/.

Required shape:

request_id: req-2026-001
kind: new-node | split-node | generalize-node | missing-dependency | lean-bridge
requested_by: <agent name>
created_at: "ISO-8601 timestamp"
target_kind: <node kind>
proposed_id: <candidate stable id>
proposed_title: <one-line title>
summary: <one sentence>
reason: |
  Why existing nodes are insufficient.
proposed_statement: |
  The most general useful form of the proposed content.
proposed_uses:
  - existing.node.id
source_justification: |
  Source or mathematical reason this should be a reusable node.

Request files are proposals. They are not admitted mathematical truth.

Agent Checklist For Node Work

Search existing nodes before creating a new one:

rg -n "<keyword>|<alternate term>" docs/knowledge

Choose one node per reusable mathematical object.
Keep machine metadata in YAML and mathematics in the Markdown body.
Use docs/knowledge/staged/ for uncertain or extracted content.
Put disagreements, gaps, and uncertainty in reviews/ or requests/.
Run structural checks after edits:

uv run python -m tools.knowledge.check docs/knowledge

If the generated site matters, publish and inspect:

uv run python -m tools.knowledge.publish docs/knowledge /tmp/mdblueprint-site

If code changed, run tests:

uv run --extra dev python -m pytest -q

Deterministic Boundary

This project relies on a strict boundary:

LLMs can propose and review.
Python decides structure.
Humans admit mathematical truth.

That means:

A staged node is not admitted truth.
A review report is evidence, not an automatic merge.
graph.json and HTML output are generated artifacts.
Stable ids may appear in URLs, anchors, and machine data, but generated UI should prefer titles.
Dependency graph display uses dependency -> dependent, even though internal graph edges store dependent -> dependency.

Verification Before Committing

For documentation-only changes:

uv run --extra dev python -m pytest -q
git diff --check

For generic documentation, skills, or tooling changes, also run the domain-neutrality audit:

uv run --extra dev python -m pytest tests/test_domain_neutrality.py -q

This audit allows domain fixtures only under docs/knowledge/** and tests/fixtures/**.

For node or publisher changes:

uv run python -m tools.knowledge.check docs/knowledge
uv run python -m tools.knowledge.publish docs/knowledge /tmp/mdblueprint-site
uv run --extra browser python -m tools.knowledge.render_check /tmp/mdblueprint-site
uv run --extra dev python -m pytest -q
git diff --check

For publisher, graph, math rendering, or Lean-link changes that could affect a real knowledge base, also run the real-library gate:

uv run --extra browser python -m tools.knowledge.econcslib_gate --render-mode smoke

Do not mark publisher or graph issues complete unless this real-library gate passes, or unless the remaining failure is recorded as an explicit blocking external-data issue.

For Lean-linked changes:

uv run python -m tools.knowledge.check docs/knowledge
uv run python -m tools.knowledge.check docs/knowledge --strict-lean-git

Use --lean-root path/to/lean/project only for one-off checks when the project does not yet have lean.repositories config.

Troubleshooting

missing dependency

: A node lists a uses id that does not exist. Search existing nodes, fix the id, or create a staged request for the missing dependency.

dependency cycle

: The uses relation is circular. Split statements or remove an incorrect dependency.

node in staged/ has admitted status

: Staged files must use staged or needs_* statuses. Admission is a separate workflow.

forbidden operational heading in body

: Move process notes into YAML, reviews/, or requests/. Node bodies are for mathematics only.

unknown macro \Foo; declare it in math.macros

: Fix the macro spelling or declare Foo under math.macros in docs/knowledge/mdblueprint.yml.

raw TeX delimiter remains after browser rendering

: A formula was not rendered by KaTeX. Check delimiter balance, project delimiter config, and browser render-check output.

external-theorem must have lean.modules and lean.declarations filled

: External theorem nodes must point to existing Lean modules and declarations.

Lean repository not specified

: Add lean.repository to the node or configure lean.default_repository in docs/knowledge/mdblueprint.yml.

ambiguous Lean declaration

: Replace the short declaration name with a fully qualified Lean declaration name.

Lean repository has uncommitted or untracked files

: Commit or clean the configured Lean repository before release publishing, or rerun with --strict-lean-git to make this an error in CI.

Current Status

The core implementation phases are complete:

Deterministic parser, validator, DAG, graph.json, and static site
Lean declaration indexing and mechanical reference prechecks
Agent contracts and report schemas
Staged-to-admitted workflow with review and generality gates
Leanblueprint-style publisher with title-first navigation, keyword pages, theorem wrappers, proof folding, and Graphviz dependency views

The test suite is the source of truth for current coverage.

Name		Name	Last commit message	Last commit date
.github/workflows		.github/workflows
docs		docs
examples		examples
skills		skills
tests		tests
tools		tools
.gitignore		.gitignore
AGENTS.md		AGENTS.md
CLAUDE.md		CLAUDE.md
README.md		README.md
pyproject.toml		pyproject.toml
uv.lock		uv.lock

Latest commit

History

Folders and files

Repository files navigation

mdblueprint

Agent Entry Points

What This Tool Owns

Install

Quickstart For Humans

Development Commands

GitHub Sync Contract

Command Reference

EconCSLib Relationship

Project Config

Repository Structure

Using Skills

The Node Model

Valid Kinds And Statuses

Human Workflow

1. Add Or Edit An Admitted Node

2. Draft A Candidate Node

3. Connect A Node To Lean

4. Publish The Website

AI And Agent Instructions

Universal Agent Contract

Global Permissions

Global Prohibitions

Source-to-MD Contract

Statement Or Definition Verifier Contract

Proof Verifier Contract

MD-to-Lean Generator Contract

External-Theorem Admission Contract

MD-Lean Alignment Verifier Contract

Admission Referee Contract

Request File Contract

Agent Checklist For Node Work

Deterministic Boundary

Verification Before Committing

Troubleshooting

Current Status

About

Resources

Stars

Watchers

Forks

Releases

Packages

Contributors

Languages