---
name: human-review
description: >-
  Prepare and guide human inspection of an Autoform roadmap or formalization
  through its Obsidian graph and rendered blueprint site. Use when a person wants
  to browse, approve, reject, or discuss scope, dependencies, progress, source
  links, or Lean artifacts visually; do not substitute an autonomous agent
  verdict for the human's judgment.
---

# Prepare a human review

Inspect the repository without changing mathematical content. Require an
existing Autoform vault and site configuration; hand missing infrastructure to
Setup. Keep the Markdown vault as the source of truth and regenerate only
derived review views.

Regenerate the review views from `<PROJECT>`: validate the blueprint, refresh
the Mermaid graph with `autoform-visualize` so Obsidian shows current
dependencies, render the site source, then strict-build the site. Follow the
publication sequence in the [CLI reference](../../autoform_cli/README.md#commands),
but omit `--require-declarations`: review happens while statements are still
unformalized, and a missing declaration is something for the reviewer to see
rather than a reason to refuse to render.

Stop on structural failures and present them before asking for mathematical
judgment. For vault review, point the user to `blueprint/README.md`, coverage,
chapter pages, and `blueprint/dependencies.md` in Obsidian. For browser review,
run `autoform dashboard <PROJECT> --site-dir site` so the same site deployed to
GitHub Pages is served on loopback with local-only live claim badges. Provide
the overview, including its progress summary, plus the project graph, relevant
chapter graph, and node-neighborhood links.

Guide the review from coarse to fine: declared scope and exclusions, milestone
book, landing-page progress summary, cross-chapter graph, chapter graph, then
individual node and Lean-source links. Record each human decision as `approve`, `revise`, or
`block`, with the exact page or node and rationale. Separate validator output
from the person's judgment. Do not silently apply requested revisions: hand
mathematical-plan changes and Lean implementation changes to Roadmap, which
records the decision and retracts the affected article so Formalize takes it up
under the [revision contract](../../autoform_cli/README.md#revision-contract),
and autonomous rubric scoring to Agent Review.

Treat the landing page's `Scoped roadmap` percentage as completion among
formalizable leaf targets that are fully proved, including every dependency
recursively. This requires proofs for theorems and bodies for definitions. A
target marked `mathlib: true` follows the authored status contract; the marker
is an author assertion, not audit verification that the declaration is in
Mathlib. Treat the percentage never as whole-source completion. Read the
adjacent declared source coverage and its linked coverage contract before
making scope claims. A statement-only theorem remains incomplete whether it is
blocked or ready to prove. In a project that allows open statements, a
conditionally proved target, whose proof rests on an open statement without a
recorded Lean proof, is not complete either: it is never fully proved, so it
counts toward the percentage's total but not its completed share, as does
every target that depends on it. Present it as conditional, naming the open
statements in its `Assumes` row, never as proved or sorry-free.