Making proofs morph, not snap — four fixes to the animation engine

[ibenian]

Over the last few PRs we went on a focused hunt to make AlgeBench's proof animations morph smoothly instead of snapping. The engine tweens one step of a derivation into the next — Manim-style — so a learner watches algebra move rather than hard-cut between frames. We found four distinct "glitches," and the fun part is that they all turned out to be the same bug wearing four different costumes.

Here's the story, the challenges, and the fixes. 🎬

Screen.Recording.2026-07-10.at.7.52.47.PM.mov

Screen.Recording.2026-07-10.at.8.01.25.PM.mov

---

The one principle behind all of it

Every visible glyph must carry a stable identity tied to the semantic graph. If it does, the engine tweens it from its old pose to its new pose. If it doesn't, it pops.

Under the hood the morph is a FLIP animation keyed on data-n:

• the renderer wraps each glyph in \htmlData{n=<id>}{…},
• KaTeX turns that into data-n="<id>" on the DOM span,
• the engine matches glyphs across two steps by that id — same id → glide, new id → fade in, vanished id → fade out,
• and a cross-step rebase (a GumTree-style tree match) threads ids so a sub-expression that persists keeps its id even as the structure around it changes.

Every bug below is a glyph that should have had a stable identity — and didn't.

---

1. The integral sign snapped — #451

Challenge. On integration steps, the ∫ sign would jump to its new position in a single frame while everything around it glided. The renderer emitted the sign as a bare glyph — \int … — with no data-n. The FLIP engine keys off ids, so an untagged sign is invisible to it: it can't tween something it can't see, so the sign just teleports on re-render.

Fix. Give each ∫ its own stable id, derived from the integral node: \htmlData{n=<node>__int}{\int}. Because that id is threaded through the rebase like any other, a persisting integral now keeps its sign and glides; a new one fades in. Multi-variable integrals (∫∫) get one id per sign.

The key idea we'd reuse everywhere: a stable id is never invented from scratch — it's derived from an id that's already stable (here, the integral node's), so it inherits the cross-step threading for free.

2. The derivative snapped — and the chain rule split it — #452

Challenge. Same disease on d/dx: the two d glyphs and the variable in \frac{d}{dx} were bare, so a persisting derivative snapped. It was most visible on the chain rule step, where d/dt splits into d/dh · dh/dt and the pieces teleported into place.

Fix, with a twist. The two ds are pure notation (no graph node), so they get a synthetic id scoped to the derivative. But the variable t is a real graph node — so its glyph should link to that node's id, not an invented one. A reviewer rightly pushed on this, and linking to the node had a bonus: the t in d/dt now resolves to its term on hover ("Time, the independent variable…").

The subtlety: the same x node can be both the operand and the variable (d/dx x²). Naively emitting the node twice would produce a duplicate data-n, which breaks the morph. So the variable glyph is occurrence-scoped to its derivative (t____deriv_2) — unique per spot, still resolves back to the term, never collides.

3. Parentheses flew, and "log" flickered — #453

Two bugs in how functions render, both surfaced on the same step.

3a — a paren flew to the wrong place. The morph matched parentheses by glyph alone — every ( was interchangeable. So when \ln(v) appeared in a step (and its ( happened to sort first in reading order), \sin's ( from the previous step matched \ln's and flew across the equation, while \sin's real paren faded in.

• First attempt: key each paren by its owner (the \sin/\ln/operator node). It fixed the flying — but regressed a different case, because a grouping paren's owner changes when the structure reorganizes ((-vₑ) moving from a fraction numerator to a factor).
• The fix that stuck: key each paren by the node it wraps (its content). \sin's ( wraps gamma, \ln's wraps v → they can't be confused; and (-vₑ) wraps the same negation node on both sides of a rewrite → it glides. Content is stable across structural moves in a way owner isn't.

3b — "log" flashed "lo" → "log". As a \log appeared, you'd see "lo" pop in and the "g" fade in a beat later. It turns out KaTeX renders a function name as a .mop that splits into a bare "lo" text node plus a separate "g" glyph span — and the engine only "saw" the real element (the "g"). Fix: wrap the whole name in one id (\htmlData{n=<node>__name}{\log}) so "log" is a single unit that fades in cleanly. Same for \sin, \cos, \ln.

4. Symmetric equations: terms flew across the ∨ — #454

The trickiest one. The quadratic's two roots — x = … + √D/2a ∨ x = … − √D/2a — split one equation into two structurally identical branches. The cross-step rebase matches nodes by content/signature, so it cheerfully paired a vanishing term from the single-equation side (the factored-away 4a² denominator's 4 and ·) with its twin in the other branch's 4ac. The glyph flew clean across the ∨.

Fix — teach the matcher about the ∨. We tag each node with the disjunction/conjunction branch it lives in exclusively (computed structurally, so it's robust to the id asymmetry where the first branch reuses old ids), and then forbid any match whose two nodes are in different branches. A new branch only inherits from the same branch of the prior state; the first branch additionally seeds from a non-disjunction predecessor — so a single equation morphs into the first solution while the rest fade in. It's a no-op for every proof that has no ∨/∧.

A nice detail from code review: the guard has to live in every phase of the matcher (top-down, bottom-up, ordered-align, recovery) — miss one and an isomorphic subtree can still sneak a cross-branch pairing through.

---

What we learned

• Every glyph needs an identity, and identity should come from meaning. The best key for a thing is what it is in the graph (the node it is, or the node it wraps), not what it looks like (its character) or where it sits (its position). Character-based and position-based keys were the root of every fly.
• KaTeX's DOM is full of surprises. Names split into "lo" + "g"; \left(…\right) becomes a .minner row; stretchy delimiters are SVGs. A lot of the work was reading the actual rendered tree rather than assuming.
• The rebase is where continuity is won or lost. Three of the four fixes ultimately live in how ids are assigned across steps. Get the correspondence right and the animation falls out for free.
• Reviewers caught the sharp edges. The owner→content pivot, the wrt-variable node link, and the "guard every phase" hardening all came from review. Worth it.

Everything is verified end-to-end in the live renderer, and each fix ships with regression tests. If you want to see them in motion, open any built-in proof in /renderproof and scrub the steps — the integral, the derivative's chain rule, the log roots of a quadratic. It should move now. ✨

PRs: #451 · #452 · #453 · #454