lra-knowledge-explorer

Theorem knowledge explorer for the Learning Real Analysis project.

Extracted from Learning-Real-Analysis/theorem-explorer/.

Contents

extract_lra_chapter.py        — LaTeX → knowledge JSON extractor
run_extraction.py             — batch extraction runner
seed_to_knowledge_json_v3_fixed6.py  — seed → knowledge.json transformer
clean_explorer.py             — cleans explorer output
knowledge-explorer.html       — interactive HTML graph viewer
real-analysis-explorer.html   — full explorer UI
preview.html                  — preview UI
PIPELINE.md                   — pipeline documentation
knowledge.json                — current knowledge graph
knowledge-seed.json           — seed data
graph-edges.json              — dependency graph edges

Running the extractor

python scripts/run_extraction.py --repos-root /path/to/workspace-containing-lra-volume-repos
python scripts/extract_model_artifacts.py --source-root /path/to/workspace-containing-lra-volume-repos
python scripts/build_to_prove.py --repos-root /path/to/workspace-containing-lra-volume-repos
python scripts/build_proof_vault_index.py --vault-root /path/to/lra-proof-vault
python scripts/extract_lean_declarations.py \
  --environment-tsv /path/to/lra-lean/build/proofs-todo-environment.tsv \
  --lean-root /path/to/lra-lean \
  --goals-json /path/to/lra-lean/build/lean-proof-goals.json

The Lean input TSV must come from the compiled environment, not a source-text approximation:

cd /path/to/lra-lean
lake build LRAIdentity
lake env lean --run scripts/DumpProofsToDo.lean \
  --prefix LRA.Identity \
  --output build/proofs-todo-environment.tsv
python /path/to/lra-knowledge-explorer/scripts/extract_lean_proof_goals.py \
  --lean-root . \
  --prefix LRA.Identity. \
  --out build/lean-proof-goals.json

Relationship to monorepo

The extraction scripts do not use the Learning-Real-Analysis monorepo as a TeX source. They require local split volume checkouts (lra-volume-i through lra-volume-viii) plus lra-governance. The canonical chapter and book list is lra-governance/docs/architecture/book-registry.json; extraction hard fails if an expected volume, chapter, notes/index.tex, or proofs/index.tex is missing.

Generated explorer records include volume, book, chapter, and section metadata. The browser UI uses that schema for the Volume → Book → Chapter → Section filters. to-prove.json uses the same metadata to power the To Prove mode.

Extraction reads live TeX files through the same volume governance inventory provider used by validators, so validation and explorer publication operate on the same canonical source set.

The HTML viewers load their generated JSON from the same directory. The Lean view consumes lean-declarations.json; the normal rebuild workflow regenerates, validates, commits, and publishes it with the other explorer artifacts. Lean records also preserve the authored declaration header and proof body, resolve source-level type and proof dependencies, and attach real before/after tactic goals queried from Lean's language server to clickable proof lines.

Verification Fields

Explorer nodes may include formal verification metadata. The UI accepts either a nested verification object or the equivalent flat fields:

• verification.system or verification_system
• verification.status or verification_status
• verification.module, lean_module, or verification_module
• verification.declaration, lean_decl, or verification_decl
• verification.source_path, lean_source, or verification_source
• verification.lean_code_b64, verification.code_b64, lean_code_b64, or verification_code_b64

The proof modal renders these records in the Verification tab. Use checked only for declarations that are accepted by the formal build without placeholders for that declaration; use statement or pending otherwise.