Skill
code-transform
Code transformation tools for repairing, simplifying, and extracting Lean proofs
@project-numinaInstall SkillResearch
Skill
/verification
Verification tools for compiling, validating, and disproving Lean theorems
Install
$ npx -y skills add project-numina/numina-lean-agent --skill verification --agent claude-codeHow it fires
How this skill gets triggered: by you, by Claude, or both.
- Fires itselfAuto-invocation. Claude auto-loads it when your prompt matches the work.Auto-invocation is when the right skill fires by itself at the right moment, driven by a FLOW.md router and a hook, instead of you invoking it by name. It is the difference between a skill being installed and a skill actually getting used.Read the full definition →
- You can call itInvoke it directly when you want it.
- Slash command
/verification
Context preview
The summary Claude sees to decide when to auto-load this skill.
Verification tools for compiling, validating, and disproving Lean theorems
SKILL.md
verification.SKILL.mdname: verification description: "Verification tools for compiling, validating, and disproving Lean theorems"
Verification Tools
Tools for verifying Lean code correctness.
Available Tools
| 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.
Ships withnumina-lean-agent
Paper | Leandex | Demo | Putnam 2025 An agent built on Claude Code for formal theorem proving tasks. We used this system to prove all 12 problems from Putnam 2025, and completed a paper-level formalization of Effective Brascamp-Lieb inequalities.
Get the whole plugin
Other skills on numina-lean-agent.
@project-numinaInstall SkillSkill
llm
LLM-assisted tools for informal proofs, proof strategy discussion, and code simplification
@project-numinaInstall SkillSkill
search
Search tools for finding Lean theorems, lemmas, and definitions in Mathlib
@project-numinaInstall SkillSkill
sorrifier
Isolates failing proof steps by replacing them with `sorry` and extracting them into standalone lemmas to modularize and decouple…
@project-numinaInstall Skill