메뉴
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 직업 분류 기준
| 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 projectKeep 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.