How zhehou/llm-isabelle works
Isabellm is a research playground for LLM-guided Isabelle/HOL proofs. The stepwise workflow accepts a goal, proposes and ranks tactics, checks them against Isabelle, and returns a proof result; the planner separately generates Isar outlines and repairs holes with verified progress. The README also describes premise selection, reranking, ATP and counterexample tools, and AFP micro-RAG. Edges reflect shown calls or README-documented capabilities; unsampled subsystems are included where documented, with links omitted when wiring is not evidenced.
Main entry points: prover.py Stepwise proof engine · driver.py Outline and fill driver · repair.py Proof repair · server.py jEdit web service
Components 21
Stepwise prover
- Prover CLI
prover/cli.py - Stepwise proof engine
prover/prover.py - Tactic strategies
prover/tactics.py
Isar planner
- Planner CLI
planner/cli.py - Outline and fill driver
planner/driver.py - Outline generation
planner/skeleton.py - Exact-context search
planner/contextual.py - Proof repair
planner/repair.py - Goal context extraction
planner/goals.py - Verified frontier
planner/frontier.py
Search and retrieval
- Proof heuristics
prover/heuristics.py - Premise selection
prover/premises.py - Theory context
prover/context.py - Tactic reranker
prover/ranker.py
Runtime integrations
- LLM routing
prover/llm.py - Isabelle proof engine
prover/isabelle_api.py - ATP and checkers
prover/strategies.py - Runtime configuration
prover/config.py - jEdit web service
isabelle_ui/server.py
Other components
- Proof author
- LLM providers
Connections 25
- Proof author → Prover CLI: submits goal
- Prover CLI → Stepwise proof engine: invokes prover
- Stepwise proof engine → Tactic strategies: generates tactics
prover/prover.py - Stepwise proof engine → LLM routing: requests candidates
prover/prover.py - Stepwise proof engine → Proof heuristics: uses heuristics
prover/prover.py - Stepwise proof engine → Premise selection: selects premises
prover/prover.py - Stepwise proof engine → Theory context: boosts facts
prover/prover.py - Stepwise proof engine → Tactic reranker: ranks candidates
prover/prover.py - Stepwise proof engine → Isabelle proof engine: checks proof steps
prover/prover.py - Stepwise proof engine → ATP and checkers: uses proof tools
prover/prover.py - LLM routing → LLM providers: routes generation
- Proof author → Planner CLI: requests outline
- Planner CLI → Outline and fill driver: starts planning
- Outline and fill driver → Outline generation: generates outlines
planner/driver.py - Outline and fill driver → Exact-context search: fills holes
planner/driver.py - Outline and fill driver → Proof repair: repairs proof
planner/driver.py - Outline and fill driver → Goal context extraction: extracts goal context
planner/driver.py - Outline and fill driver → Verified frontier: tracks progress
planner/driver.py - Outline and fill driver → Isabelle proof engine: verifies proof
planner/driver.py - Exact-context search → Stepwise proof engine: reuses generators
planner/contextual.py - Proof repair → Goal context extraction: uses goal details
planner/repair.py - Proof repair → Verified frontier: checks progress
planner/repair.py - jEdit web service → Stepwise proof engine: calls prover
isabelle_ui/server.py - jEdit web service → Outline and fill driver: calls planner
isabelle_ui/server.py - Stepwise proof engine → Runtime configuration: reads settings
prover/prover.py