用 Codex 或 Claude 帮你安装 复制这段 Prompt,粘贴到 Codex、Claude 或其他助手里,让它检查 Skill 页面并帮你完成安装。
直接命令不会经过审查 Prompt;运行前请先检查来源。
npx skills add https://github.com/project-numina/numina-lean-agent --skill llm命令会保持在同一行。复制前请横向滚动并检查完整内容。
想先保存到本地?可下载 SkillsMP 当前能够提供的文件。
正在显示 SKILL.md
基于 SOC 职业分类
| 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.