Orchestrates the Leanstral prover to generate and kernel-check Lean 4 proof terms.
npx skills add https://github.com/ZK-Theory/TDL --skill lean-proof-zk-theory
Please help me install this Agent Skill. Skill: lean-proof Source: https://github.com/ZK-Theory/TDL/tree/main/.agents/skills/lean-proof Command: npx skills add https://github.com/ZK-Theory/TDL --skill lean-proof-zk-theory
vibe -p "<prompt>" --agent lean --trust in programmatic mode, avoiding interactive sessions that hang under automation. - Generate-compile-heal loop: Lifts frozen theorem statements verbatim, generates proof terms, kernel-checks with lake env lean or named lake build targets, and re-prompts the prover with exact kernel error messages (capped at ~5 iterations). - Mandatory preflight and guardrails: Smoke-tests authentication before any proof work, enforces frozen signatures, keeps defs out of promoted files, and records prover_identity and prover_data_exposure provenance honestly. - Use Case: Running a Lean proof spike such as S2.MaxAriBound — the orchestrator decomposes a hard lemma into helper lemmas, lets Leanstral fill them, verifies the axiom set with #print axioms, and reports an obstruction with a pre-authored fallback if the prover cannot close the goal. ## Quick Start Ask the agent to drive the Leanstral prover to generate and kernel-check a Lean 4 proof for a frozen theorem statement, starting with the mandatory smoke-test preflight.High-intent search queries and answers about installing and using this skill.
Invoke vibe in programmatic mode with `vibe -p "<prompt>" --agent lean --trust` after setting the MISTRAL_API_KEY environment variable. The bare positional prompt opens an interactive session that blocks on stdin and hangs under automation.
Kernel-check standalone files with `lake env lean <file>`, or integrate into the project and build a named target like `lake build S2.MaxAriBound`. Confirm the axiom set with `#print axioms` — a clean set contains propext, Classical.choice, and Quot.sound with no sorryAx.
The vibe CLI's stored config key can lapse independently of flags, producing the Invalid API key error. Run the mandatory smoke-test preflight first; on auth failure, stop and escalate to the owner rather than hunting keys or editing .env files.
PowerShell 5.1's `Out-File -Encoding utf8` emits a UTF-8 BOM that Lean rejects at position 1:0. Write files BOM-free using `[IO.File]::WriteAllText(path, text, (New-Object Text.UTF8Encoding $false))`.
Decompose the hard lemma into helper lemmas and re-prompt with exact kernel error messages, capped at about five iterations. If it still resists, deliver the pre-authored fallback with an obstruction report — never hand-write the proof term.
No. Statement signatures are frozen by the statement author and countersigned in statement_source. A signature that would need to change is an escalation to the statement author, never a re-encoding by the orchestrator.
r-irbeClassify Lean 4 theorem proofs as vacuous, tautological, or placeholder.
real-caseSupersede an accepted Architecture Decision Record by pairing it with a successor via the adr MCP tool.
JoernStoehlerStandardize standalone math.tex documents with YAML frontmatter and LaTeX statements.
fmhallProvide Lean 4 tactic alternatives for proofs without Mathlib.