菜单
Expand the valid but complicated proofs in a module to have more detailed steps, so that they can be found by forced proof search.
用 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.
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.
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.
| name | Explicate |
| description | Expand the valid but complicated proofs in a module to have more detailed steps, so that they can be found by forced proof search. |
Sometimes, we have a valid proof, in the sense that its certificate can be verified. But the proof is too complicated, in the sense that the prover cannot re-discover the proof with forced search if we were to lose the certificate. In this situation, we often want to "explicate" the proof, ie to add more detailed steps to the .ac file so that the prover is able to re-discover the proof.
We can only explicate when we have a valid proof. So, the first step is to check that we have valid proofs in the module that we want to explicate.
acorn check MODULENAME
Note that module names can be single words like "add_ordered_group" or dot-separated like "comm_ring.binomial".
If the check fails, we won't be able to explicate.
The next step is to figure out which lines we need to explicate. Run forced proof search with --fail-fast. Once we find a line that fails, we'll know we need to explicate it.
acorn verify MODULENAME --force-search --fail-fast
If there's a crash or an internal error, that's a bug in Acorn. We should stop explicating and tell the user there's an Acorn bug.
If this command works, we're done with this module.
If we find a line that can't be found by forced search, make note of the line number and go to the next step.
Once we know a line that cannot be found by forced search, select the proof to see its detail.
acorn select MODULENAME LINENUMBER
This will show a list of statements and reasons. Statements that come from:
can be used for explication. Insert these statements in the .ac file in front of the line we are explicating. (If the line has a by block, instead insert the statements at the end of the by block.)
Don't delete statements! You should only have to add new statements.
After modifying the file, run a verify of the whole module to ensure the new lines can all be proven, and update the certs.
acorn verify MODULENAME
If this doesn't verify, something was bad with the code we inserted wrong. Try fixing it so that it verifies.
If it does verify, we can repeat. Try forced proof search on this module again, to see if any lines still need explication.
When you are done explicating a module, run forced proof search on that module. Ideally, it should succeed. If it doesn't, try explicating again.