Menu
Verification tools for compiling, validating, and disproving Lean theorems
The review-first prompt is selected by default. You can switch to a direct command or download a local copy.
Read SKILL.md and any companion files shown by SkillsMP before deciding whether to install.
Install with Codex or Claude Copy this prompt, paste it into Codex, Claude, or another assistant, and let it review the skill page and install it for you.
A direct command skips the review prompt. Inspect the source before running it.
npx skills add https://github.com/project-numina/numina-lean-agent --skill verificationThe command stays on one line. Scroll horizontally to inspect it before copying.
Prefer a local copy? Download the files currently available to SkillsMP.
Showing SKILL.md
Based on SOC occupation classification
| name | verification |
| description | Verification tools for compiling, validating, and disproving Lean theorems |
Tools for verifying Lean code correctness.
| Tool | Purpose | When to use |
|---|---|---|
| lean-check | Compile a Lean file and report errors (local, no API key) | First step to validate any proof attempt |
| axle verify-proof | Validate a proof matches a formal statement | When you need to confirm a proof proves exactly the right theorem |
| axle disprove | Attempt to disprove theorems by proving negation | Before investing effort in a proof, check if the conjecture is false |
For full parameters and examples, read the corresponding reference-<tool>.md file in this directory.