Imported from Zhen-WushuiLingchun/lean_visualization (
AGENTS.md). Install upstream withnpx skills add Zhen-WushuiLingchun/lean_visualization. Copyright stays with the author.
AGENTS.md — ProofFlow
Guidance for every agent (human or AI) working in this repository. Read fully before editing.
The architecture is in docs/ARCHITECTURE.md; the related-work decision is in docs/SURVEY.md.
1. What ProofFlow is
ProofFlow turns a built Lean 4 project into an auditable proof workflow: a left-to-right DAG whose
sources are the axioms a project rests on (Lean's three standard axioms, sorryAx, Lean.ofReduceBool
from native_decide, and any user-declared axiom), whose interior is definitions and lemmas, and whose
sinks are the project's final theorems. Every node carries its full transitive trust profile (axioms,
sorry, native_decide, unsafe/partial/extern) and can be re-verified in-app by exporting its
dependency closure with leanexport and replaying it through the official kernel and the independent
kernels bundled with the toolchain (lean4lean, nanoda, con-leche, con-ron, leanchecker-paranoid).
The audience is someone auditing a formalization (their own, a collaborator's, or an AI-generated one): "what does this theorem really rest on, and does an independent checker agree?"
Non-goals (v1)
- Tactic-level proof trees inside a single proof (Paperproof does this).
- Semantic review workflow / confidence attributes (Lean Atlas does this).
- Hosting all of Mathlib as a browsable site (keithadler/leanviz does this).
- Editing Lean code. ProofFlow is read-only over
.oleanfiles plus source display.
2. Ground truth about the toolchain (verified 2026-09-27 on Windows 11)
- Toolchain used for development and the example project:
leanprover/lean4:v4.35.0-rc3(Mathlib master is on the same version). Installed viaelan;~/.elan/binmust be on PATH. - Binaries bundled in that toolchain's
bin/:lean,lake,leanexport(the formerlean4export, NDJSON export format 3.1.0),leanchecker(kernel replay;--fresh,--from-export <file.ndjson>),leanchecker-paranoid,lean4lean,nanoda_bin,con-leche,con-ron. Exact CLI usage of each checker is recorded indocs/CHECKERS.md. Read it; do not guess flags. lake check(v4.35+) builds, exports, replays through the kernel and fails on non-standard axioms;lake check --paranoidalso runs every bundled external checker. ProofFlow's per-node verification is the per-declaration analogue of this.- Since v4.32,
ConstantInfo.value?on theorems returnsnoneunless called asci.value? (allowOpaque := true). Always useallowOpaque := truewhen collecting proof dependencies. Lean.collectAxiomsis correct but slow when called per declaration (rebuilds its cache each call). The extractor must do one shared-cache traversal (seeleanprover-community/axiom-audit).collectAxiomsMany(lean4 PR #14157) is not merged; do not depend on it.- Known core bug:
#print axiomsunder-reports axioms of imported inductives on v4.35.0-rc3 (lean4 issue #15226). Our own SCC traversal overgetUsedConstantsis not affected.examples/toyreproduces it (Toy.Signed,Toy.signed_trivial);lean/CrossCheck.leanproves the extractor is the correct side, andexamples/toy/expected/README.mddocuments the two expected mismatches. Do not "fix" the extractor to agree with#print axioms. - Flag taints (
unsafe/partial/extern/implementedBy) are NOT propagated out of core packages (Init,Std,Lean,Lake) by default, otherwise every theorem aboutNatwould beextern-tainted throughNat.add.--core-flag-taintsrestores the literal rule. Axiom taints always propagate. native_decideon v4.35 mints a per-use axiom<decl>._native.native_decide.ax_i_j; on ≤ 4.34 it usesLean.ofReduceBool, which rests onLean.trustCompiler. All three are classifiednativeDecide.leanexport <Module> -- <decl>exports only that declaration and its transitive closure (verified: 183 lines for a trivial theorem, 1 s).leanchecker --from-export file.ndjsonprintsLean default kernel accepts the solutionand exits 0 on success (verified, 0.2 s).lake env <cmd>runs<cmd>withLEAN_PATHset so the project's.oleans and the toolchain binaries are found. Every Lean-side invocation from the server goes throughlake env.- Lean scripts are executed as
lake env lean --run <file.lean> -- <args>;main : List String → IO Unitreceives<args>(verified). The script mustinitSearchPath (← findSysroot)and thenimportModules #[{module :=Root}] {} 0` to obtain the environment. - Windows paths: prefer forward slashes internally; quote every path passed to a subprocess; never rely
on a POSIX shell. Node
child_process.spawnwith an args array,shell: false. - Mathlib-scale measurements (2026-09-27, Windows 11, one machine): a real 50-module project over
Mathlib on Lean 4.33 (
YM_and_EYM/formal/lean): import of 4648 modules 10 s, 34 104 reachable constants, 760 k kernel edges, 4507 nodes written, 29 s total,graph.json7.8 MB.examples/mathlib-demoon Lean 4.35.0-rc3 + Mathlibv4.35.0-rc3: extract 15 s;verify MathlibDemo.sqrt_two_irrationalwith all six checkers: closure 10 410 declarations, export 41 MB in 6.5 s, every checker accepted in 1.5 to 7.2 s, 23 s wall. - Toolchains before v4.35 ship
leancheckeronly (verified: v4.33.0 has noleanexport, no external kernels, and itsleancheckerhas no--from-export). Theleanchecker-modulefallback (module replay from.olean) is the only kernel-level check available there.leanprover/lean4exporthas a tag per toolchain version, so building it on demand is a possible future upgrade. - Verified end to end on 2026-09-27:
proofflow extractonexamples/toyin 4 s (288 nodes),proofflow verify Toy.cleanMain --checkers allaccepted by all six checkers in 1.4 s, and the viewer drove a live verification through the API (SSE) in headless Chrome.con-leche/con-rondecline (exit 2) any closure containingsorryAxor a custom axiom; that is expected and shown as a grey dash.
3. Repository layout
AGENTS.md this file
README.md user-facing intro (EN + ZH summary)
docs/SURVEY.md related tools and why ProofFlow exists
docs/ARCHITECTURE.md components, data flow, API, layout, scale strategy
docs/CHECKERS.md verified CLI usage of leanexport/leanchecker/lean4lean/nanoda/con-leche/con-ron
docs/VERIFICATION.md what each verification level proves and does not prove
lean/Extract.lean extractor script (no Lake dependency for users; run via `lake env lean --run`)
lean/README.md
examples/toy/ small Lean project exercising every trust case; golden test fixture
packages/schema/ @proofflow/schema — zod schemas + TS types for graph.json and verify results
packages/server/ @proofflow/server — CLI (`proofflow`), Hono HTTP API, extraction + verification
packages/web/ @proofflow/web — Vite + React + @xyflow/react + elkjs viewer
Package manager: pnpm (workspace). Node ≥ 22. TypeScript strict, ESM only, "type": "module".
4. Contracts every package must respect
graph.jsonis the only interface between Lean and TypeScript. Its shape is defined once inpackages/schema/src/graph.ts. The extractor writes it; the server validates it with zod before serving; the web app types against it. Never add a field on one side without adding it to the schema first.- Edge direction is dependency → dependent.
sourceis the thing used,targetis the thing that uses it. Axioms are sources in the viewer (column 0):graph.jsonmay still record what a local axiom's statement mentions indeps.stmt(e.g.Toy.oraclementionsNat), and the viewer drops those edges. Final theorems have no outgoing edges (within the project). This is the workflow reading order (left → right) and it is fixed. - Node id = fully qualified Lean name as printed by
Name.toString(with «» escaping when needed). - Trust profile is computed in the extractor, transitively, once.
axiomsis the complete transitive axiom set.taintsis derived (see schema) and is also transitive. The web app must not recompute transitive closures over the full graph; it may compute them over the currently displayed cone. - Verification results are per (declaration, exportHash) and cached under
.proofflow/cache/in the audited project. A result for one checker never implies another checker's result. - Local vs external. Declarations whose module belongs to the audited project's own libraries are
isLocal: trueand fully expanded. External declarations directly referenced by local ones are emitted as boundary nodes with their own trust profile butdepsComplete: falseunless--expand-external.
5. Verification levels (the "can this node be verified by its predecessors" feature)
| Level | Name | What runs | What it proves |
|---|---|---|---|
| L0 | Trust profile | nothing (from graph.json) | which axioms/sorry/native_decide/unsafe the node transitively rests on |
| L1 | Kernel replay | leanexport Root -- decl → leanchecker --from-export |
the node and its whole closure re-typecheck in a fresh environment with Lean's own kernel (catches environment hacking) |
| L2 | Independent kernels | same export → lean4lean, nanoda_bin, con-leche, con-ron, leanchecker-paranoid |
independent implementations agree; disagreement is a finding, not noise |
A node is shown green only when L1 is accepted and every requested L2 checker accepted. L0 taints are
displayed regardless (a sorry-tainted theorem can still be kernel-accepted; that is exactly what the
audience needs to see).
6. Working rules
- Run the real pipeline on
examples/toybefore claiming anything works:pnpm build && pnpm proofflow extract --project examples/toythenpnpm proofflow serve --project examples/toy. - Tests:
pnpm testat the root runs every package's vitest suite. Lean-side golden tests live inpackages/server/test/and compare extractor output onexamples/toyagainstexamples/toy/expected/. If you change extractor output intentionally, regenerate goldens and explain why in the commit. - Never mark a checker as "accepted" on a non-zero exit code. Unknown exit codes are
error, notrejected. - Long subprocesses (extraction, checkers) must have timeouts and must stream logs; the UI must never hang.
- Do not add dependencies casually. Allowed:
zod,hono,@hono/node-server,commander,child_process(built-in),@xyflow/react,elkjs,graphology(+graphology-dag,graphology-types),react,react-dom,vite,@vitejs/plugin-react,vitest,jsdom,@testing-library/react,typescript,tsx,@types/*. Anything else needs a one-line justification in the commit message. The rootpnpm-lock.yamlis shared: add a dependency by editing the package'spackage.jsonand runningpnpm installfrom the repo root once. - Ports: the server listens on
4870by default; the Vite dev server on5173proxies/apito it. - Line endings are LF everywhere (
.gitattributesenforces it). - Keep Lean code dependency-free (only
import Leanplus the audited project's root). It must compile on any toolchain ≥ v4.28; if you use an API introduced later, guard it or document the floor bump. - Style: no em-dashes in user-facing UI strings; short sentences; English identifiers and comments.
- Commit messages: imperative subject ≤ 72 chars, body explains why. Sign as instructed by the harness.
7. Ownership map (initial build, 2026-09-27)
| Area | Owner | Deliverable |
|---|---|---|
| Contracts, survey, architecture, audit | lead (Claude Fable 5.1) | AGENTS.md, docs/*, packages/schema |
| Lean extractor + toy project + goldens | subagent A (Opus 5.5) | lean/Extract.lean, examples/toy, examples/toy/expected/graph.json |
| Server, CLI, verification orchestration | subagent B (Opus 5.5) | packages/server |
| Web viewer | subagent C (Opus 5.5) | packages/web |
The lead audits every deliverable against sections 4 and 5 before it is merged.
8. Audit checklist (run before any release or after touching the extractor/checkers)
pnpm build && pnpm testgreen in all three packages.PROOFFLOW_INTEGRATION=1 pnpm --filter @proofflow/server testgreen (golden equality onexamples/toyplus a real six-checker run).- In
examples/toy:lake env lean --run ../../lean/CrossCheck.lean -- expected/graph.json Toyexits 0 (every node agrees with a cache-free axiom walk; the two documented#print axiomsmismatches are expected). proofflow verify Toy.cleanMain --checkers all→ accepted;proofflow verify Toy.everything --checkers all→ partial with con-leche/con-ron declined and the four kernels accepted.- Open the viewer on
examples/toy, selectToy.everything, runVerify (all checkers), confirm the table matches step 4 and the badge is a grey dash (declined), not green.
