acornprover

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.

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.

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.

Use when asked to migrate to a feature flag or roll out a manifest-gated acornlib certificate/build-cache or proof-format change. This skill covers feature-flag migrations, including the state-machine workflow for verifier, proof, and cache migrations.

Use when asked to profile Acorn prover or verifier performance, investigate where time is spent, or generate a top-down runtime breakdown from `perf` or `samply`.

Use when a theorem or goal ought to prove but the prover fails in acornlib or an issue repro. Classify whether the failure is a shallow explosion or an interactive timeout/activation-cap case that should reproduce as `--shallow` exhaustion, then narrow it to a local repro and, once approved, turn a single positive `verify_succeeds` case into an mdtest.

Use when a proof/module verifies in baseline mode but reproving under a prover-affecting feature flag fails. Add explicit proof detail based on the working baseline proof until `cargo run --features <feature> -- verify ...` succeeds.

Regenerate the Acorn website documentation by running the Acorn CLI docs generator, especially the auto-generated library reference under docs/library, from the adjacent acornlib checkout. Use when working in the acornprover.org repository and the user asks to update, refresh, regenerate, or publish docs generated by acorn docs.