Skip to content

native-lean-workflow-surface.md

Latest commit

 

History

History
278 lines (215 loc) · 14.7 KB

native-lean-workflow-surface.md

File metadata and controls

278 lines (215 loc) · 14.7 KB
Raw

Native Lean Workflow Surface

This document summarizes the native Lean workflow/tooling contract that now drives LeanFlow.

Canonical Workflow IDs

LeanFlow normalizes the public Lean workflow commands to these internal workflow IDs:

  • prove
    • /prove
    • /autoprove
  • formalize
    • /formalize
    • /autoformalize
  • draft
  • review
  • checkpoint
  • refactor
  • golf

The auto-prefixed forms are aliases only. They are not separate runtimes or policy bundles.

/formalize and /autoformalize require a project-local .tex source, .pdf source, or directory containing a TeX project. The resolver prepares document preflight artifacts, a generated supplemental blueprint skill, and an active Lean target file before the native runner starts. Directory inputs are resolved to a main TeX source and record included .tex, bibliography, PDF, figure, and TeX support files in the manifest. LaTeX preflight recognizes standard theorem environments plus custom declarations from \newtheorem, \declaretheorem, \newmdtheoremenv, \mdtheorem, \spnewtheorem, and \newtcbtheorem; it also handles plain-TeX \profess...\endprofess blocks and nearby proof bodies. Once the drafting pass has a compilable sorry skeleton and only statement/source approval is missing, the native runner starts the configured independent verifier pass over the source document, blueprint, and Lean draft. By default this uses the managed reviewer agent; auxiliary.blueprint_verification can instead route advisory review to a model/RPC provider, Codex CLI, Claude Code, or deterministic local-only checks. auxiliary.autoformalizer_verification separately controls advisory review around the deterministic autoformalization handoff verifier. After review approval and deterministic local/Lean checks, the formalizer gets one focused generated-file organization pass, then exits; proof filling waits for an explicit user-run /prove SomeFile.lean or /prove. /prove SomeFile.lean auto-attaches the generated skill when SomeFile.lean has a nearby Blueprint.md; users can also pass --additional-skill path/to/SKILL.md.

Specs Are The Contract

The canonical contract lives in markdown-backed specs under:

  • leanflow_specs/workflows/
  • leanflow_specs/workers/

Workflow specs currently shipped:

  • prove
  • formalize
  • draft
  • review
  • refactor
  • golf
  • checkpoint
  • doctor
  • search

Dormant worker specs currently shipped:

  • proof-repair
  • proof-golfer
  • axiom-eliminator
  • sorry-filler-deep

Skills remain the routing layer, but the prompt builder, doctor, router, and Lean tools all read the same spec metadata. leanflow_cli/lean_workflow_specs.py validates alias collisions and unknown worker references in tests.

Native Lean And Document Tools

The repo-owned Lean tool surface is defined in tools/lean_tool.py and backed by leanflow_cli/lean_services.py.

Document formalization also exposes read_pdf and formalization_document_inspect from tools/document_tool.py, backed by leanflow_cli/formalization_documents.py. read_pdf is the obvious model-facing tool for extracting text from project-local PDF papers. formalization_document_inspect inspects project-local .tex and .pdf sources, extracts LaTeX sections, standard and custom theorem-like environments, adjacent proof excerpts, and PDF text metadata when local tools are available, and reports degraded extraction reasons.

Managed queue turns allow new helper declarations that directly support the assigned theorem. The edit guards preserve existing theorem/lemma/example statements and restore edits to pre-existing non-assigned declarations or future queue items.

  • lean_capabilities
    • project validity
    • lean / lake / elan binary availability
    • MCP/LSP tool discovery
    • search-provider availability
    • helper availability
    • worker availability
    • degraded-mode reasons
  • lean_inspect
    • diagnostics
    • goals
    • sorry_count
    • project_sorry_count
    • blocker_kind
    • queue_items
    • capability_report
  • lean_verify
    • mode=file_exact|module|project
    • file_exact is the acceptance path for file-scoped theorem turns
  • lean_search
    • mode=auto|local|semantic|type-pattern|natural-language
    • MCP-first provider selection with rg/Mathlib fallback
    • provider provenance in attempted_providers and per-result metadata
    • explicit degraded_reasons when semantic providers are missing or skipped
  • lean_proof_context
    • theorem-local context retrieval from the managed automation backend
    • returns theorem statement, original proof, hypotheses, in-scope names, namespace, and optional similar proofs
    • not a replacement for lean_inspect goals
    • prefers local declaration-range stabilization when the active file already contains the target declaration
    • falls back to a local declaration slice when proof-auto reports theorem_not_found or another backend-side context miss
    • keeps proof-auto MCP enabled after a theorem-lookup miss; only transport or systemic backend failures are sticky-disabled for the current run
  • lean_multi_attempt
    • theorem-local screening for 2-6 concrete tactic candidates at one file position
  • lean_auto_search
    • theorem-local automated proof candidate search after proof context or concrete local evidence exists
  • apply_verified_patch
    • compatibility path for one atomic Lean patch, pre-edit checkpoint, and immediate verification payload
    • managed queue workflows normally use patch/write_file, because the runner verifies successful edits before advancing the queue
  • lean_sorries
    • project/file-scoped sorry findings with line number and declaration name
  • lean_axioms
    • best-effort #print axioms wrapper
    • returns axioms, custom_axioms, classical, and choice
    • dispatches native worker presets
    • uses file locks when owner/delegation context is available
    • returns a structured plan instead of hard-failing when delegation is unavailable

These tools are available through the lean, leanflow-native, and leanflow-native-swarm toolsets.

LeanFlow installs and manages the Lean MCP backends by default:

  • lean-lsp-mcp
    • role: primary-state-search
    • exposes diagnostics, goals, search, state/premise/hover/outline discovery, and tactic attempt screening
    • configured with LEAN_REPL=true and local Loogle on Linux/macOS/WSL
    • prefers local acceleration first when toolchain-compatible with the active project, then public remote Lean search fallbacks, then native project/Mathlib search
  • lean-proof-auto-mcp
    • role: secondary-automation-context
    • used through native wrappers, with local fallback when backend theorem lookup misses a declaration visible in the current file
  • lean-explore
    • role: semantic-declaration-search
    • lean_search prefers the local LeanExplore backend when lean-explore[local] is installed and lean-explore data fetch has prepared the index
    • lean_search can fall back to the hosted LeanExplore API when LEANEXPLORE_API_KEY is set
    • the managed MCP server is still configured disabled by default; enable it for MCP search_summary/getter tools, or switch it to a prepared local backend after fetching LeanExplore data

Those servers exist to back the native tools above. Raw mcp_* tools are not part of the normal native Lean workflow surface.

Queueing, Routing, And Workers

The file/declaration queue is still the core execution model. The runner now supplements it with a structured route decision:

  • inputs
    • workflow kind
    • queue item
    • blocker kind
    • attempt count
    • search exhaustion
    • capability/degraded-mode state
  • outputs
    • skill_name
    • route_action
    • reason

Queue items are enriched with:

  • line numbers
  • blocker signatures
  • search hints
  • verification gates

Project Prove Manager

/prove SomeFile.lean enters the existing file-scoped theorem queue directly. /prove with no file enters the project prove manager first.

The manager is intentionally a thin scheduler above the file queue:

  • it only chooses the next file
  • it does not edit Lean files itself
  • it does not replace theorem-level queueing, diagnostics, failed-attempt tracking, or verification gates
  • it delegates each assigned file back to the same path used by /prove SomeFile.lean

Startup behavior:

  1. The workflow resolver normalizes /prove and /autoprove to prove.
  2. The native runner checks whether the command contains an explicit .lean file.
  3. If there is no explicit file, the project prove manager scans project Lean files for sorry.
  4. Candidate files are summarized with:
    • relative label
    • absolute path
    • module name
    • sorry_count
    • line_count
    • declaration count
    • pending declaration names, source excerpts, and per-declaration difficulty scores
    • hint and worked-example counts
    • full source for small files, or selected header/import/hint/theorem excerpts for larger files
    • direct and transitive candidate-file imports/dependents
    • direct and transitive project-file imports/dependents
    • imported_by_count
    • import_count
  5. A deterministic fallback queue is built from candidate-to-candidate dependency importance, unresolved candidate dependencies, project-wide downstream importance, theorem difficulty, first-pending-declaration difficulty, sorry count, length, declaration count, and stable path order.
  6. The configured LLM is asked to reorder the bounded candidate list using the same policy and the provided source context, with competition-style theorem names treated as harder and hinted/worked-example-heavy files treated as easier.
  7. The LLM response is accepted only as JSON-like file labels that match known candidates; missing fallback files are appended, and deterministic dependency/difficulty buckets remain guardrails around the model order.
  8. The first file is assigned by setting LEANFLOW_NATIVE_ACTIVE_FILE.
  9. The normal file-scoped theorem queue takes over.

Continuation behavior:

  • after the active file verifies, the manager records it as completed
  • the manager refreshes candidates from the current filesystem, so solved files disappear from the queue
  • if candidates remain, the next file is assigned
  • if no candidates remain, the project prove queue is complete

Parallelism policy:

  • default /prove uses one managed agent and one assigned file at a time
  • parallel agents are only enabled by explicit user flags such as --agents 3
  • explicit file workflows with a file argument continue to force file-local handling instead of becoming project scheduling runs

Document Formalization Preflight

/formalize docs/paper.tex, /autoformalize docs/paper.pdf, and /autoformalize docs/paper-directory normalize to the same formalize workflow.

Before launch, the resolver:

  1. requires the source path to exist inside the active LeanFlow project
  2. accepts .tex, .pdf, or a directory containing a TeX project
  3. for directory inputs, deterministically selects the main .tex entrypoint, collects included .tex files, bibliography files, and local assets, and fails ambiguous roots with a clear error
  4. creates .leanflow/workflow-state/formalization/<source>/manifest.json
  5. creates .leanflow/workflow-state/formalization/<source>/extracted.txt
  6. creates .leanflow/workflow-state/formalization/<source>/blueprint.md
  7. creates an active Lean target file if it does not already exist
  8. records both the original request path and the selected source document in workflow state
  9. sets LEANFLOW_WORKFLOW_CONTEXT so the runner prompt includes the document contract
  10. sets LEANFLOW_NATIVE_ACTIVE_FILE to the generated target file so statement/source review and later proof work have a stable Lean entrypoint

The generated Markdown blueprint is the default planning artifact. If a project already has blueprint/ or leanblueprint available, the planner should keep that TeX blueprint in sync with the generated declaration names and dependency labels.

Doctor And MCP

leanflow doctor now uses the same capability layer as the Lean workflows.

Supported modes:

  • all
  • env
  • mcp
  • search
  • migrate
  • cleanup

Useful commands:

leanflow doctor
leanflow doctor mcp --json
leanflow doctor search --json
leanflow mcp bootstrap lean
leanflow mcp status
leanflow mcp status --json

leanflow mcp status reports server role, managed/install/config health, connection state, registered tools, local Loogle/REPL power-mode status, public remote fallback policy, and sampling counters.

leanflow mcp bootstrap lean is the idempotent repair/setup command for the managed Lean MCP stack.

Power-mode details:

  • Local Loogle avoids the public Loogle rate limit and is attempted on Linux/macOS/WSL. First local setup may take 5-10 minutes and about 2GB of disk. If it is cold or unavailable, public remote Lean search fallback remains enabled.
  • REPL mode makes line-based lean_multi_attempt faster after the project has a built repl binary. leanflow project init attempts safe setup, prints progress for lake update repl and lake build repl, and continues with LSP fallback if setup fails.
  • LeanExplore local mode is preferred when available. Install with pip install 'leanflow-agent[lean-explore]' or pip install 'lean-explore[local]', run lean-explore data fetch, then use lean_search mode=semantic|natural-language. Hosted API mode remains credential-gated through LEANEXPLORE_API_KEY.

For persistent sampling audit logs, set mcp_servers.<name>.sampling.audit_jsonl: true in ~/.leanflow/config.yaml. The default path is ~/.leanflow/logs/mcp-sampling.jsonl, with audit_jsonl_path available as an override.

Persisted Workflow State

Native Lean workflows now persist more than logs and checkpoints.

Relevant files under .leanflow/workflow-state/ include:

  • live_status.json
  • activity/
  • runs/
  • file_locks.json
  • outcomes.jsonl

For project-scoped /prove, live_status.json stores project_prove_manager, project_prove_file_queue, project_prove_completed_files, project_prove_plan_source, and project_prove_plan_reason alongside the normal active-file, queue, diagnostics, build, route, checkpoint, and provider/model fields.

The activity JSONL stream records project prove-manager events:

  • project-prove-file-queue-planned
  • project-prove-file-assigned
  • project-prove-file-queue-empty
  • project-prove-file-queue-complete

project-prove-file-queue-planned contains the candidate metrics and final ordered file labels. project-prove-file-assigned contains the assigned file, absolute path, remaining queue, plan source, and plan reason. These events are intended to be machine-readable enough for detailed inspection and offline training trace curation.

outcomes.jsonl records route decisions so later cycles and resumed sessions can reuse prior blocker classifications and search/repair history.