| name | algebench-prove |
| description | Interactively build a research-grounded mathematical proof or derivation — research the topic on the web (opt-in per source), confirm the derivation path, generate CAS-verified proof JSON via the algebench-proof-anim pipeline, save it under proofs/domains, and open it on the /prove page. Pass --research to stop at a copy-paste research summary + recommended prompt and (optionally) open a pre-filled Derive tab. |
| triggers | ["algebench-prove","build a proof","prove this","research and prove","derive a proof","research a derivation"] |
| args | [topic] [--research] |
AlgeBench Prove
Take a user from "I want to prove/derive X" to a rendered, research-grounded proof
on the /prove page. This skill researches the topic on the web, confirms the
derivation path with the user, generates the CAS-verified trajectory using the
algebench-proof-anim pipeline (derive.py → report.py --save-builtin), saves it
under proofs/domains/<domain>/<name>.json, and opens /prove?id=<domain>/<name>.
See docs/shareable-proof-animations.md
for the proof data model and .agents/skills/algebench-proof-anim/SKILL.md
for the generation pipeline this skill reuses. Follow AGENTS.md
for repo-wide rules (branch before changes, the user merges PRs, committer trailer).
Operating principle: guide, don't guess
This skill is interactive. At every decision point, present concrete options via
AskUserQuestion (recommended default first), then act on the answer. Do the research
before proposing a path, and confirm the math (endpoints + route) before generating —
never silently invent a whole derivation and dump a file. The intermediate steps come
from derive.py (ProofCompletionExpert + CAS), not from hand-guessing.
Modes
- Full mode (default): research → confirm → save-location → generate → open on
/prove.
--research mode: research → summarize → stop before generation. Output a
copy-paste recommended prompt + documentation, then offer to open /prove with the
Derive tab pre-filled (prompt + doc) but not started. See Step 6.
Workflow
1. Pick the target
If the user already named a proof/derivation, restate it and move on. Otherwise
AskUserQuestion: What do you want to prove or derive? Offer a few concrete examples
if useful (e.g. "the quadratic formula", "the normalization constant of the normal
distribution", "the Tsiolkovsky rocket equation").
2. Understand the domain, then offer research
Identify the math domain (algebra, calculus, physics, quantum, series, …) and the
rough context. Then propose reliable sources and let the user opt in/out per source
(or pick all) via AskUserQuestion with multiSelect: true. A good default set:
- Wikipedia — broad, well-referenced overviews
- Wolfram MathWorld — precise definitions and identities
- ProofWiki — formal, step-by-step proofs
- nLab — higher/abstract-math framing
- arXiv / lecture notes — for research-level or applied derivations
- Encyclopedia of Mathematics (EoM) — authoritative reference
Recommend the 2–3 that best fit the topic (put them first). Respect the user's
selection exactly — research only the chosen sources.
3. Do the research
Use WebSearch / WebFetch against the chosen sources only. Enforce reliable-source
discipline and capture citations as you go — for each, record:
key — short stable id (e.g. wiki-normal-dist, mathworld-gaussian)type — online | textbook | paper | videotext — full human-readable citation (title + source + URL)relevance — one line on what it contributed
Prioritize correctness: every definition, identity, and proof outline you carry
forward must be mathematically accurate and traceable to a source.
4. Summarize the research
Give a concise, structured summary — definitions, key results/identities, and the
candidate derivation(s) — without writing out the step-by-step algebra yet. Include
the citations. This summary doubles as the documentation used later (Steps 6 & 8).
5. Confirm the derivation path (verbally, no algebra)
AskUserQuestion: confirm what is derived from what and the high-level route — in
words, not equations. Name the start and target explicitly (this is what the
generator needs). If the research surfaced multiple valid starting points or alternative
routes (e.g. Gaussian integral via polar coordinates vs. via the Gamma function),
present them as options and let the user choose. Do not proceed until start → target and
the route are confirmed.
6. --research short-circuit
If --research was passed, stop here — generate nothing. Output, clearly labeled:
Recommended derivation prompt: a single natural-language prompt that would drive
proof_from_prompt / derive.py (names the start, target, and route).Documentation: the structured research write-up from Step 4 (definitions, key
identities, route, citations) — sized for the Derive tab (≤ 5000 chars).
Then AskUserQuestion: Open /prove with the Derive tab pre-filled (prompt + docs), ready
for you to click Derive?
If yes, hand off via the draft-prefill mechanism (local/DEBUG only). The draft is a
markdown file /tmp/algebench/proofdraft/<docid>.md — the documentation as markdown,
with optional YAML-style frontmatter carrying prompt and domain:
DRAFTS=/tmp/algebench/proofdraft
mkdir -p "$DRAFTS"
DOCID="$(python3 -c 'import uuid;print(uuid.uuid4().hex[:16])')"
cat > "$DRAFTS/$DOCID.md" <<EOF
---
prompt: <recommended derivation prompt — single line>
domain: <domain>
---
<the documentation as markdown — definitions, key identities, route, citations>
EOF
./algebench --prove --debug --server-only --port <p> --skip-tour
The page opens on the Derive tab with the prompt, documentation, and domain filled in
but not run — the user reviews and clicks Derive themselves. Skip all remaining steps.
Why a .md file + token (not URL params): the documentation can be long, and passing a
caller-supplied path would be a local-file-read vector. The skill writes the draft under a
random docid in a fixed, server-owned dir; only the opaque token rides in the URL. The
server validates the token (^[A-Za-z0-9_-]{6,64}$), reads <docid>.md itself, and
parses the frontmatter — gated to DEBUG so the public /prove never reads local files.
7. Choose the save location (collision-checked)
Recommend a kebab-case slug and its path: proofs/domains/<domain>/<name>.json.
Slug rules (satisfy the store, the builder, and the /prove deep-link at once):
- lowercase letters/digits/hyphens only, two segments
<domain>/<name>
domain 2–32 chars, name 3–64 chars; no reserved names (index, new, admin,
api, null, undefined)
Check the name is free before offering it — never overwrite:
test -e proofs/domains/<domain>/<name>.json && echo "TAKEN (seed)"
test -e .proof-store/domains/<domain>/<name>.json && echo "TAKEN (store)"
AskUserQuestion to confirm the default slug. If the user offers a different name,
re-run the collision check on that name before accepting it. Loop until the chosen name
is free.
8. Generate the proof (reuse the algebench-proof-anim pipeline)
Always use derive.py to produce the trajectory — it runs the expert and CAS-verifies
each step. Do not hand-author the chain. (Needs GEMINI_API_KEY in .env.local.)
Feed it the confirmed prompt (or explicit start → target) from Step 5:
./run.sh scripts/proof_animation/derive.py --prompt "<confirmed prompt>" \
--domain <domain> --out <scratch>/anim.json
./run.sh scripts/proof_animation/derive.py "<START>" "<TARGET>" \
--title "<Title>" --domain <domain> --out <scratch>/anim.json
jq '[.]' <scratch>/anim.json > <scratch>/list.json
./run.sh scripts/proof_animation/report.py --from-file <scratch>/list.json \
--save-builtin <domain>/<name>
Review the printed steps. If the math is wrong, adjust the prompt/endpoints and
re-run — never hand-edit expr_latex or the saved JSON (a malformed step fails
assert_well_formed; re-derive instead). This writes proofs/domains/<domain>/<name>.json.
9. Open it on /prove
Launch the /prove server and open the saved proof by id (/prove?id= finds both the
committed seed and the runtime store):
./algebench --prove --server-only --port <p> --skip-tour
Verify with the preview tools that the page loaded that proof (Derive is not needed here —
the proof opens as its own tab). Screenshot as proof it rendered.
10. Confirm or iterate
Final AskUserQuestion: Looks good / revise a step / rename / build another? Loop back
to the relevant step. On "revise", re-derive (Step 8) with an adjusted prompt/endpoints —
don't hand-edit. On "rename", re-run the collision check (Step 7) and re-save.
Submission & review lifecycle (what to tell users)
There are two ways a proof reaches the public /prove catalog. Know both, and
explain the second to any user who builds a derivation in the Derive tab and wants it
published:
- Authored + committed (this skill): you write
proofs/domains/<domain>/<name>.json, it's merged via PR (the user merges), and it
ships as a built-in — canonical, always in Browse.
- Public submit-for-review (no accounts, the
/prove Derive tab): a user derives a
proof and clicks ↑ Submit. It lands in a review queue, not in Browse, until a
maintainer promotes it. This is the path to describe below.
The submission lifecycle:
- Submit. In Derive, ↑ Submit → a dialog asks for a new unique name
(
<domain>/<name>, checked live against built-ins + published + other pending
submissions, so it can never collide). On success the proof + its package (the derive
prompt, documentation, references) is written to the review queue
(proof-submissions/…), never to proofs/.
- Pending (under review). The submission is hidden from Browse by default. It's
reachable two ways: the direct link
/prove?id=<domain>/<name>, or Browse → tick
"Show proofs under review" (it shows with an under review badge). Nothing is public
yet.
- Promotion. A maintainer reviews and promotes it into
proofs/ (an admin/offline
step). Only then does it appear in Browse for everyone. Once promoted it's a normal
published proof — clone-only (see the key rules below).
The edit key — tell users to save it. On submit (and after every update) the thank-you
dialog shows a one-time edit key (with a Copy button). It's the only handle to edit a
pending submission and is never stored server-side / never shown again. It's a hash of
the proof content, so it rotates whenever the proof changes.
To use the key: open the pending submission (direct link, or Browse with the toggle) →
click ✎ Edit → paste the key → it loads into Derive in edit mode (prompt + docs
restored, Submit becomes ↑ Update). Adjust / Rederive → ↑ Update saves in place and
shows the new rotated key.
Two rules to state plainly:
- Edit only while pending. The ✎ Edit button exists only while the submission is in
the review queue. Once approved/promoted, the key no longer edits anything — the proof
is clone-only (⧉ Clone → tweak → submit under a new name). Lose the key while it's
still pending and you're also down to cloning.
- Versioning. In the submit dialog, keeping the same name updates your pending
submission; typing a new name files a separate version for review. One Derive
session can spawn several named versions, each with its own key.
If a user "can't find" their submission, it's almost always the default-hidden queue — point
them at the direct link or the Show proofs under review toggle; the proof is safe.
Notes
- Correct path is
proofs/domains/<domain>/<name>.json — a single domains/<domain>
segment (not domains/domains/...).
/prove?id= serves the committed seed and the runtime .proof-store, deduped by id
(seed wins on a clash).- Safety: proof JSON is rendered as untrusted — KaTeX with trust limited to
\htmlData, human text via textContent, strict CSP. Generate via the script so the
\htmlData term ids stay valid and the animation morphs correctly.
- DEBUG for prefill: the Step-6 Derive-tab prefill only works when the server runs with
--debug (it's DEBUG-gated so the public /prove never reads local files). The id=
open in Step 9 does not need debug.
- Never commit the generated proof unless the user asks — offer it, and let them decide
(the user merges PRs; see AGENTS.md).
