formal-methods
Verify proofs, check theorem correctness, and solve satisfiability problems using Lean 4, Coq, and Z3 SMT solver. Use when the user asks to prove theorems, verify mathematical proofs, check logical satisfiability, or work with proof assistants.
来源信息
- 仓库
- Prismer-AI/Prismer
- 最近来源活动
- 2026年3月19日 07:49
- 检测到的 SKILL.md 语言
- 英语
- 星标
- 794
- 分支
- 38
安装方式
默认使用会先检查来源的 Prompt；你也可以切换为直接命令，或下载本地副本。
检查来源文件
决定是否安装前，请先阅读 SKILL.md，以及 SkillsMP 当前展示的配套文件。
文件资源管理器
3 个文件正在显示 SKILL.md
SKILL.md
来源说明 · 只读预览- name
- formal-methods
- description
- Verify proofs, check theorem correctness, and solve satisfiability problems using Lean 4, Coq, and Z3 SMT solver. Use when the user asks to prove theorems, verify mathematical proofs, check logical satisfiability, or work with proof assistants.
- _source
- Canonical source at /skills/formal-methods/SKILL.md
# formal-methods
Formal verification tools for the academic workspace. Type-check Lean 4 proofs, verify Coq theories, and solve SMT satisfiability problems with Z3.
## Process
1. **Check availability** — Use `prover_status` to see which provers are installed
2. **Write proof** — Draft your Lean/Coq code or SMT formula
3. **Verify** — Use `lean_check`, `coq_check`, or `z3_solve` to verify
4. **Iterate** — Fix errors based on output and re-check
## Tools
- `lean_check` — Type-check Lean 4 code. Params: `code` (required), `filename`
- `coq_check` — Check a Coq proof. Params: `code` (required), `filename`
- `coq_compile` — Compile Coq to `.vo` object file. Params: `code` (required), `filename`
- `z3_solve` — Solve SMT-LIB2 formula. Params: `formula` (required)
- `prover_status` — Check available provers and versions. No params.
**Example:**
```json
{ "code": "theorem add_comm (a b : Nat) : a + b = b + a := Nat.add_comm a b" }
```
See [canonical skill](/skills/formal-methods/SKILL.md) for full tool documentation and parameter details.
在 GitHub 查看