Agent Skills
› Prismer-AI/Prismer
› formal-methods
formal-methods
GitHub提供形式化验证工具，支持使用 Lean 4、Coq 和 Z3 SMT 求解器进行定理证明、数学证明验证及可满足性检查。适用于学术工作区中的逻辑与数学推理任务。
触发场景
用户请求证明定理
验证数学证明正确性
检查逻辑可满足性
使用证明辅助工具
安装
npx skills add Prismer-AI/Prismer --skill formal-methods -g -y
SKILL.md
Frontmatter
{
"name": "formal-methods",
"_source": "Canonical source at \/skills\/formal-methods\/SKILL.md",
"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."
}
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
- Check availability — Use
prover_statusto see which provers are installed - Write proof — Draft your Lean/Coq code or SMT formula
- Verify — Use
lean_check,coq_check, orz3_solveto verify - Iterate — Fix errors based on output and re-check
Tools
lean_check— Type-check Lean 4 code. Params:code(required),filenamecoq_check— Check a Coq proof. Params:code(required),filenamecoq_compile— Compile Coq to.voobject file. Params:code(required),filenamez3_solve— Solve SMT-LIB2 formula. Params:formula(required)prover_status— Check available provers and versions. No params.
Example:
{ "code": "theorem add_comm (a b : Nat) : a + b = b + a := Nat.add_comm a b" }
See canonical skill for full tool documentation and parameter details.
版本历史
- 2dbe71f 当前 2026-08-20 10:21
