Lean Prover¶

lean_prover — Lean 4 theorem proving with 7 cognitive proof strategies.

Cluster: Uncategorised | Type: component | MCP Tools: 31

Overview¶

Interactive Lean 4 theorem prover with informal proof sketch generation, tactic search, theory management, and persistent session tracking. Provides a full 27-op MCP interface for integrating Lean-based formal verification into G6 agent pipelines.

Production verification caveats

Run lean_prover_lean_status before relying on Lean-backed proof results. For production-critical gates, require readiness.ga_ready=true and an empty readiness.actions list. Treat verification_status="generated" or verified=false as unverified source only; generated definitions, lemmas, proof sketches, and formalizations must pass lean_prover_check_proof before being used as proofs. verification_status="proved" is not sufficient by itself for policy approval; callers must also have verified=true or reference a stored theorem record that was verified by Lean.

The external reliability label follows a kernel-evidence invariant: reliability_label="verified" is emitted only when the Lean kernel re-verified the proof (G6_LEAN_PROVER_KERNEL_REVERIFY, default on), a proof artifact hash is present, and no sorry/admit-class tactic was used. If kernel re-verification is explicitly disabled, a search strategy's self-reported success is downgraded to qualified-draft (never verified); a missing or failed Lean toolchain fail-closes to blocked-escalated. This invariant is pinned by tests/mvp/lean_prover/test_verified_requires_kernel_invariant.py.

Use lean_prover_replay_artifact and lean_prover_enforce_policy before allowing artifacts into medium, high, regulated, or safety-critical workflows. Session and theorem state persists to ~/.g6/lean_prover.sqlite3 by default; set LEAN_PROVER_DB_PATH to a managed writable path in production deployments. Mathlib-dependent proofs require a configured Lake/Mathlib project. Pantograph and research grounding are optional and status-reported; batch Lean verification can still work without them.

Lean proving is an advanced reliability gate, not the recommended first-10-minute onboarding path for non-technical users. For launch pilots and "vibe coder" workflows, expose it through templates, examples, or higher-level verification recipes rather than asking users to debug Lean/Lake/Mathlib setup directly.

When to use:

Formally verifying safety properties or algorithm correctness in Lean 4
Generating human-readable informal proof sketches before formalisation
Building a persistent theorem library for iterative formal verification

Example:

from mvp.lean_prover import LeanProverBlock, LeanProverInput

block = LeanProverBlock()
result = block.infer(LeanProverInput(op="prove_theorem", theorem="∀ n : ℕ, n + 0 = n"))
# result.is_ok() -> True; result.value -> LeanProverOutput with verified=True, proof

Works well with: formal_methods, cegis, csf

Public API¶

`LeanProverBlock(AIBlock[LeanProverInput, LeanProverOutput, dict])`¶

Orchestrating block for Lean 4 theorem proving with 7 cognitive strategies.

Methods:

`infer(input: LeanProverInput) -> Result[LeanProverOutput]`¶

Route by input.op to the appropriate handler.

`capability_plan(op: str, params: dict) -> CapabilityResolution`¶

`heavy_dependency_status() -> list[dict]`¶

`list_patterns() -> dict[str, object]`¶

Return the applied deterministic-reliability pattern catalog.

`LeanProverPatternRuntime`¶

Deterministic false-verified self-check over an emitted output (no LLM, no I/O).

Methods:

`validate_output(result: Any) -> list[str]`¶

Return false-verified / internal-consistency violations of an emitted output.

`assert_consistent(result: Any) -> Any`¶

Live-path guard: raise if the emitted output is a false-verified envelope.

`LeanProverInput(BaseModel)`¶

Field	Type	Default
`op`	`LeanProverOp`	required
`theorem`	`str`	''
`proof`	`str`	''
`tactic`	`str`	''
`session_id`	`str`	''
`name`	`str`	''
`type_sig`	`str`	''
`body`	`str`	''
`docstring`	`str`	''
`imports`	`str`	''
`fields_json`	`str`	''
`nl_statement`	`str`	''
`target_domain`	`str`	''
`interpretation_index`	`int`	-1
`strategy`	`str`	''
`config_json`	`str`	''
`proof_id`	`str`	''
`proof_id_2`	`str`	''
`verification_status`	`str`	''
`verified`	`bool`	False
`risk_level`	`str`	'medium'
`query`	`str`	''
`top_k`	`int`	10
`session_data_json`	`str`	''

`LeanProverOutput(BaseModel)`¶

Field	Type	Default
`op`	`str`	''
`ok`	`bool`	True
`proof`	`str`	''
`verified`	`bool`	False
`verification_status`	`str`	'unverified'
`verifier`	`str`	''
`artifact_hash`	`str`	''
`artifact_json`	`str`	''
`proof_state_json`	`str`	''
`tactics`	`list[str]`	Field(default_factory=list)
`lean_source`	`str`	''
`definition_name`	`str`	''
`nl_explanation`	`str`	''
`nl_sketch`	`str`	''
`formalized`	`str`	''
`well_formedness_json`	`str`	''
`research_hits_json`	`str`	''
`candidate_interpretations`	`list[str]`	Field(default_factory=list)
`strategy_used`	`str`	''
`strategies_ranked_json`	`str`	''
`failure_analysis`	`str`	''
`comparison_json`	`str`	''
`policy_decision`	`str`	''
`policy_json`	`str`	''
`theorems_json`	`str`	''
`session_id`	`str`	''
`session_data_json`	`str`	''
`status_json`	`str`	''
`records`	`list[dict]`	Field(default_factory=list)
`message`	`str`	''
`error`	`str`	''
`elapsed_sec`	`float`	0.0
`metadata`	`dict`	Field(default_factory=dict)
`degraded`	`bool`	False
`degradation_reason`	`str \\| None`	None

`LeanProverSkill`¶

Field	Type	Default
`name`	`str`	required
`pattern_slug`	`str`	required
`description`	`str`	required
`executable`	`bool`	required
`mechanism`	`str`	required
`capabilities`	`tuple[str, ...]`	required
`triggers`	`tuple[str, ...]`	required
`risk_notes`	`tuple[str, ...]`	required

Methods:

`compact() -> dict[str, Any]`¶

`LeanProverSkillCatalog`¶

Maps each applied pattern slug to a lean_prover deterministic-reliability skill.

Methods:

`list_skills() -> list[LeanProverSkill]`¶

`executable_skills() -> list[LeanProverSkill]`¶

`get(slug: str) -> LeanProverSkill | None`¶

Functions¶

`applied_agentic_patterns() -> list[dict[str, Any]]`¶

Return compact metadata for lean_prover-applied vendored patterns.

`get_skill_catalog() -> LeanProverSkillCatalog`¶

MCP Tools¶

Operation	Source
`ops`	lean_prover_mcp
`help`	lean_prover_mcp
`prove_theorem`	lean_prover_mcp
`prove_step`	lean_prover_mcp
`check_proof`	lean_prover_mcp
`search_tactics`	lean_prover_mcp
`prove_interactive`	lean_prover_mcp
`create_definition`	lean_prover_mcp
`create_lemma`	lean_prover_mcp
`import_theory`	lean_prover_mcp
`search_library`	lean_prover_mcp
`extend_theory`	lean_prover_mcp
`formalize`	lean_prover_mcp
`explain_proof`	lean_prover_mcp
`informal_sketch`	lean_prover_mcp
`ground_research`	lean_prover_mcp
`configure_strategy`	lean_prover_mcp
`get_proof_state`	lean_prover_mcp
`analyze_failure`	lean_prover_mcp
`compare_proofs`	lean_prover_mcp
`enforce_policy`	lean_prover_mcp
`save_session`	lean_prover_mcp
`load_session`	lean_prover_mcp
`list_theorems`	lean_prover_mcp
`get_theorem`	lean_prover_mcp
`replay_artifact`	lean_prover_mcp
`lean_status`	lean_prover_mcp
`search`	lean_prover_mcp
`info`	lean_prover_mcp
`capabilities`	lean_prover_mcp
`list_patterns`	lean_prover_mcp

Lean Prover¶

Overview¶

Public API¶

LeanProverBlock(AIBlock[LeanProverInput, LeanProverOutput, dict])¶

infer(input: LeanProverInput) -> Result[LeanProverOutput]¶

capability_plan(op: str, params: dict) -> CapabilityResolution¶

heavy_dependency_status() -> list[dict]¶

list_patterns() -> dict[str, object]¶

LeanProverPatternRuntime¶

validate_output(result: Any) -> list[str]¶

assert_consistent(result: Any) -> Any¶

LeanProverInput(BaseModel)¶

LeanProverOutput(BaseModel)¶

LeanProverSkill¶

compact() -> dict[str, Any]¶

LeanProverSkillCatalog¶

list_skills() -> list[LeanProverSkill]¶

executable_skills() -> list[LeanProverSkill]¶

get(slug: str) -> LeanProverSkill | None¶

Functions¶

applied_agentic_patterns() -> list[dict[str, Any]]¶

get_skill_catalog() -> LeanProverSkillCatalog¶

MCP Tools¶

`LeanProverBlock(AIBlock[LeanProverInput, LeanProverOutput, dict])`¶

`infer(input: LeanProverInput) -> Result[LeanProverOutput]`¶

`capability_plan(op: str, params: dict) -> CapabilityResolution`¶

`heavy_dependency_status() -> list[dict]`¶

`list_patterns() -> dict[str, object]`¶

`LeanProverPatternRuntime`¶

`validate_output(result: Any) -> list[str]`¶

`assert_consistent(result: Any) -> Any`¶

`LeanProverInput(BaseModel)`¶

`LeanProverOutput(BaseModel)`¶

`LeanProverSkill`¶

`compact() -> dict[str, Any]`¶

`LeanProverSkillCatalog`¶

`list_skills() -> list[LeanProverSkill]`¶

`executable_skills() -> list[LeanProverSkill]`¶

`get(slug: str) -> LeanProverSkill | None`¶

`applied_agentic_patterns() -> list[dict[str, Any]]`¶

`get_skill_catalog() -> LeanProverSkillCatalog`¶