菜单
Install and set up the Acorn theorem prover CLI. Use when the environment doesn't have Acorn installed or when the user needs to set up Acorn for the first time.
用 Codex 或 Claude 帮你安装 复制这段 Prompt，粘贴到 Codex、Claude 或其他助手里，让它检查 Skill 页面并帮你完成安装。
基于 SOC 职业分类
Keep named project roadmaps under `projects/PROJECT/` updated as structured execution queues, execute roadmap work, and run projects continuously through hourly PR-aware scheduled cycles. Use when the user asks to plan or update a project roadmap, add roadmap items, maintain long-term mathematical project plans, explicitly asks to "work on a project", or asks to work on a project "in continuous mode". The default current project is `translate-mathlib`.
Refactor Acornlib modules without changing the mathematics, especially moving definitions/theorems between files or packages. Use this when imports, package interfaces, file paths, or certificates need to be updated while preserving existing proofs; prefer `acorn check` over `acorn verify` and repair stale certificate references directly.
Use when a theorem is mathematically true but difficult to formalize directly, especially when proof search times out, the statement is large, or the proof needs helper lemmas, dependency research, or structured decomposition.
Expand the valid but complicated proofs in a module to have more detailed steps, so that they can be found by forced proof search.
Fix Acornlib pull request merge conflicts, especially conflicts only in generated `build/` files. Use when the user gives a PR id or URL, or asks to resolve merge conflicts in this repo: take conflicted build files from `master`, run `acorn verify` from the repo root to regenerate/update build artifacts, then commit and push the resolved PR branch when appropriate.
Remove explicit theorem citations from Acorn proofs by replacing each citation with local proof steps while keeping `acorn verify` passing after every attempted change. By default, make a full pass over the current `acorn citations` list unless the user explicitly narrows the scope. Use when the user asks to inline cited theorems, reduce `acorn citations` output, or improve proof style without changing the theorem being proved.
| name | Acorn Installation |
| description | Install and set up the Acorn theorem prover CLI. Use when the environment doesn't have Acorn installed or when the user needs to set up Acorn for the first time. |
This skill helps install the Acorn theorem prover CLI in various environments.
Simply run the installation script:
bash .claude/skills/acorn-installation/install-acorn.sh
The script will:
~/.local/bin/acornOnce installed, you can verify Acorn proofs by running:
acorn
This should be run after every change to ensure proofs are verifiable.
When this skill is invoked:
bash .claude/skills/acorn-installation/install-acorn.shacorn to verify proofs in the current project