Menu
LLM-assisted tools for informal proofs, proof strategy discussion, and code simplification
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 llmThe command stays on one line. Scroll horizontally to inspect it before copying.
Prefer a local copy? Download the files currently available to SkillsMP.
Based on SOC occupation classification
Showing SKILL.md
| name | llm |
| description | LLM-assisted tools for informal proofs, proof strategy discussion, and code simplification |
LLM-assisted tools for theorem proving support. All scripts are in skills/cli/.
| Tool | Purpose | When to use |
|---|---|---|
| informal-prover | Generate and verify step-by-step math solutions in a loop | When you want an LLM to attempt a full solution with auto-verification |
| discussion-partner | Free-form discussion about proof strategies or Lean code | When you are stuck and want high-level strategic advice |
| code-golf | Shorten and simplify an existing Lean proof via Gemini | After a proof works, to get a more elegant version |
For full parameters and examples, read the corresponding reference-<tool>.md file in this directory.