| name | algebench-proof-anim |
| description | Research a mathematical derivation with the user, generate a shareable AlgeBench proof animation JSON, and launch the app to show it rendering. Interactive and AskUserQuestion-driven at every decision point. |
| triggers | ["proof anim","proof animation","make a proof animation","shareable proof","render proof","algebench-proof-anim"] |
AlgeBench Proof Animation Builder
Turn a mathematical derivation into a shareable, embeddable proof animation
that lives in this repo under proofs/domains/<domain>/<name>.json and renders at
…/renderproof?builtin=<domain>/<name>.
See docs/shareable-proof-animations.md
for the full system design. This skill produces the built-in proof JSON and shows
it rendering.
Operating principle: guide, don't guess
This skill is interactive. At each decision point present concrete options via
AskUserQuestion (recommended default first), then act on the answer. Never
silently invent the whole derivation and dump a file — confirm the math first.
Workflow
1. Decide the endpoints (don't write the steps yourself)
Figure out the start and target LaTeX (and, optionally, the intent) — NOT
the intermediate steps. The intermediate steps come from derive.py, which runs
the ProofCompletionExpert + CAS so they're model-derived and machine-checked, not
hand-guessed.
Confirm with AskUserQuestion, e.g.:
- Is this the right start → target? (e.g.
ax^2+bx+c=0 → the quadratic formula)
- Which domain parser? (algebra, calculus, physics, … — affects LaTeX parsing)
2. Name it
AskUserQuestion to confirm the <domain>/<name> slug. Recommend a kebab-case
default derived from the title (e.g. "Isolate a" → algebra/isolate-a). The slug
must match ^[A-Za-z0-9_-]+/[A-Za-z0-9_-]+$. Show the file path it will write:
proofs/domains/<domain>/<name>.json.
3. Generate the trajectory with derive.py, then save it
Always use the derive script to produce the trajectory — it runs the expert and
CAS-verifies each step. Do NOT hand-author the chain of expr_latex steps.
(Needs GEMINI_API_KEY in .env.local.)
./run.sh scripts/proof_animation/derive.py "<START>" "<TARGET>" \
--title "<Title>" --domain <domain> --out <scratch>/anim.json
./run.sh scripts/proof_animation/derive.py --prompt "<natural language>" --out <scratch>/anim.json
Review the generated steps (print them). If they're wrong, adjust the
endpoints/prompt and re-run derive.py — don't fix the math by hand.
derive.py --out writes a single ProofAnimation; report.py --save-builtin
wants a one-entry list. Wrap it, then build + save (parse, rebase, annotate,
CAS-grade, optional LM term descriptions):
jq '[.]' <scratch>/anim.json > <scratch>/list.json
./run.sh scripts/proof_animation/report.py --from-file <scratch>/list.json --save-builtin <domain>/<name>
This writes proofs/domains/<domain>/<name>.json. If the build errors on a
malformed step (it runs assert_well_formed), re-derive — do not hand-edit the JSON.
Fallback (no LM key, or a tiny fixed chain): you may hand-author a single-entry
ProofAnimation list and pass it straight to report.py --from-file … --save-builtin.
The shape is {title, domain, start_operation, start_justification, trajectory:{kind:"proof_trajectory", start_latex, target_latex, steps:[{operation, expr_latex, justification, change_type:"rewrite"}]}}
where each expr_latex is the FULL expression after that step. Prefer derive.py.
4. Show it live (use the right URL)
./algebench --proof <domain>/<name>
For headless verification, run ./algebench --server-only --port <p> and load the
shareable page in the preview tools:
http://localhost:<p>/renderproof?builtin=<domain>/<name> — that exact path, NOT
the app root / (the main 3D viewer), and confirm the page stayed on that URL
before screenshotting.
Report the share URL and the embed snippet (an <iframe> + the optional
embed-resizer.js script). Use the deployed host in the snippet only once the
/renderproof feature is live there.
5. Confirm or iterate
Final AskUserQuestion: Looks good / revise a step / rename / add another proof?
Loop back to the relevant step as needed. To put several proofs on one page, the
URL takes repeated params: ?builtin=algebra/isolate-a&builtin=algebra/expand-binomial.
Safety note
The renderer treats every proof JSON as untrusted: math is rendered through KaTeX
with trust limited to \htmlData, all human text via textContent, and the page
runs under a strict CSP. So a generated (or hand-edited) proof can never execute
scripts — but still generate via the script, don't hand-craft annotated LaTeX,
so the \htmlData term ids stay correct and the animation morphs properly.
