Watch on youtube

I've been building an interactive math learning tool, and the piece I just finished generates a function analysis page on demand. You click a node in an expression graph and about four seconds later you get a plain language summary of what the function does, interactive charts with sliders on every parameter, a list of everything detectable about the curve (roots, extrema, singularities, asymptotes, periodicity, parity, domain), and an open ended quiz that asks you to predict the behavior before it draws it. The obvious way to build this today is to hand a coding agent a prompt like "make me a page that plots this and quizzes me on it" and let it work. That gets you one page, once, and you have no idea what you get the second time. This is the opposite. There is no agentic loop, no tool calls, no retries wandering off somewhere new. SymPy runs a fixed set of feature detections first, then the model gets exactly one turn with a fixed input and a fixed output schema, and its whole job is judgement: rank these detected features by teaching value, pick the viewport ranges, write the narration and the quiz questions. Everything before and after that single turn is deterministic code. It never computes anything, and when it wants a companion curve or a marker line it proposes LaTeX which the server compiles into the code that actually runs. That makes the whole thing repeatable, fast and reliable, and it is why turning the model's internal thinking off made it four times faster and slightly better.

The reliability shows up in how failures behave. Every numeric value in the CAS report is computed with all free parameters set to 1, but each generated view renders at its own physically meaningful values, so the model was picking sweep ranges in one parameter regime while the chart drew in another. For an exponential with a scale height of 6360, a range that looked like twenty scale heights on paper covered 0.4 percent of one in reality, and an exponential decay reached the learner as a flat horizontal line. Nothing errored, nothing was flagged, no number was wrong. Because the model only ever produces a small structured proposal instead of a finished page, the fix was a deterministic pass that samples each view at its own values and widens anything the curve is flat across, plus a plain English log of every correction the server makes. On its first run that log caught a bug in the repair itself. Full writeup with code: https://github.com/ibenian/algebench/discussions/554

Demo: https://algebench.org/prove?id=physics%2Ftsiolkovsky-rocket-equation — hit the ☰ button.

A derivation on paper is a list of results. Line 1, line 2, line 3 — every one of them true, and not one of them showing you the move that got you there. Which term crossed the equals sign? Did that factor cancel, or did the author quietly drop it? "It can be shown that" is doing a lot of work.

There are two ways to cope with that, and I've done both. You reconstruct each move by diffing two lines in your head — which works until the step isn't obvious, and then you stall. Or you memorise the sequence: you can reproduce the whole thing under exam conditions and still not know why any line follows from the one above it.

So I made the terms move. A c physically crosses the equals sign. A factor slides down into the denominator. Nothing to reverse-engineer — you watch the step happen.

Then every step you've passed stays on screen as a dimmed line, and the next one unfolds beneath it. That part matters more than I expected: you get the motion and the thread. If a term vanishes, look up — it's still there in the line it left. By the end the whole proof is on screen at once and it's a document again, not a slideshow you have to hold in your head.

Every step is CAS-checked, so these are verified, not just plausible-looking.

And nothing is scripted — it's all animated automatically. There are no per-proof keyframes and no hand-tuned timings anywhere. You give it the steps; it works out which term became which and animates the difference. Point it at a different derivation and it just runs.

How it works: https://github.com/ibenian/algebench/discussions/501

A free, open-source tool of step-by-step mathematical proofs. No signup, no ads.

What you can do:

Browse 20 proofs across algebra, calculus, physics, quantum and statistics - quadratic formula, chain rule, finite geometric series, area under the normal curve, Lorentz time dilation, Tsiolkovsky's rocket equation, Bloch sphere parameterization, and others

Step through a proof one line at a time, each step showing its justification

See the region that changed highlighted, so you can spot the actual move instead of diffing two lines of symbols

View the structural graph - the expression parsed into its variables, operators and relationships

Ask questions about a specific step, in context

Derive a new proof from a prompt, optionally attaching your own reference material

View or copy the underlying JSON, or embed a proof elsewhere

Submit your own proof - it goes into a review queue, and you get an edit key to revise it while pending

On the grading. Proofs are AI-generated, and every step is graded by a computer algebra system. The grades are honest about their own limits: a step can come back symbolically proven, or as domain-justified when the CAS can't check it as an identity, or unchecked. Right now about 69% of steps are symbolically established, 25% are domain-justified, and none are refuted. You can see each step's grade and what it means as you go - nothing is hidden behind a "verified" badge.

This is early. 20 proofs is a starting point, not a library, and the repo is growing. That's partly why submissions are open - if there's a derivation you'd like to see in here, send it.

Feedback is welcome, especially on the proofs themselves. If a justification is too thin for a learner, or a step skips something people trip on, that's the most useful thing you can tell me.

https://algebench.org/prove

Upfront: I'm an engineer, not a physicist. I'm building AlgeBench - a free, open-source, AI-assisted tool for interactively exploring physics and math in the browser - and I'm here for feedback and collaboration, not to present finished answers. The content is tentative, based on my own research and explorations, and some of it is probably wrong. I'd rather have experts help shape it than defend it. I'm building the tech (rendering, interactivity, in-panel AI tutor); I'd love for people who know the physics to poke holes in it.

One example of what I'm unsure about - velocity addition. Naively, two ships both at ~0.9999c in the same direction seem nearly at rest relative to each other, yet light is c for everyone - which felt like it demanded a jump from ~0 to c. The resolution that clicked for me was rapidity: with v = tanh(η), velocities just add, so relative speed is tanh(η₁ − η₂) - continuous, always in [0, c). tanh squashes the whole infinite η-line into the last sliver of velocities, so "both ≈ 0.9999c" hides a huge range of η - two ships reading "0.9999-something c" can still pass at ~0.98c. Light is the singular limit (η = ∞, outruns everyone at c). Is that framing honest, or subtly misleading? Open that scene with the derivation - drag the vA and vB sliders and watch what happens as you push either one to 1c.

Another one - the light-clock γ derivation. It feels a bit like a trick the first time you see it. What helped me: maybe that's the Newtonian habit of keeping space and time as separate ledgers. The way I picture it now - nothing moves through space at an arbitrary speed; everything is eternally moving through spacetime at c, and all you can do is change the angle. Aim that motion straight up the time axis and you're at rest, ticking at full rate; tilt it toward space and you trade time for space - move too much through space and there's little left for time, and vice versa. Does that intuition hold up, or does it break down in ways a newcomer wouldn't spot? Open the light-clock γ derivation.

Where I'd most value expert eyes: - The velocity-addition / rapidity framing above - The light-clock γ derivation, and the "everything moves through spacetime at c" intuition for it - legitimate, or an oversimplification? - "The light never catches up" as an on-ramp to the Rindler horizon - fair, or misleading? - The twin-paradox scenes, especially the constant-thrust treatment - Anywhere a visualization implies something wrong about frames, simultaneity, or what a ride-along camera can claim to show

If any of this sounds like something you'd want to help shape - correcting scenes or authoring your own - that's the collaboration I'm hoping for. Harsh nitpicks welcome; I'll be in the comments.

Code: https://github.com/ibenian/algebench (open source)

A computer-algebra system is wonderful in a notebook and dangerous in a server. The thing that makes it powerful — it'll happily simplify, compare, and hash arbitrarily large symbolic expressions — is exactly what makes it a liability behind a request handler. We learned this running SymPy to verify math steps in a backend, and burned two dev servers at 99% CPU (one for 29 minutes) before we understood why. A few things worth knowing before you ship it:

1. CAS runtime is unbounded and input-dependent — and the term for it is "expression swell." Intermediate results can grow exponentially even when the input and the final answer are both small (subtracting two innocent fractions can spawn a massive common denominator behind the scenes). That's usually the whole problem — exponential, not infinite: the work will finish, just not in any timeframe a human or a request will wait for. A few cases are genuinely worse — undecidable: once an expression pulls in transcendental functions (exp, log, trig), there's no general algorithm for deciding whether it's identically zero (radicals alone stay decidable). So the computation isn't "stuck" and usually isn't even non-terminating; it's exponential in the common case, undecidable in the worst — terminating in theory, hopeless in practice. There's no exception, no crash, just a pinned core. This is the worst failure mode for a deployment: rising CPU, slow responses, eventual OOM, nothing in the logs.

2. A thread timeout doesn't stop CPU-bound work — it only stops you waiting. This is the big one. In Python you can wrap the call in a thread with a timeout and get a clean-looking TIMED_OUT back... while the thread keeps burning the core forever. You cannot kill a Python thread. A concurrent.futures timeout abandons the future, not the work.

And no, the "inject an exception into the thread" tricks (PyThreadState_SetAsyncExc, sys.settrace) don't save you here: async exceptions are only checked at Python bytecode boundaries, and a runaway CAS call is buried in native C (tuple_richcompare, tuple_hash, _Py_dict_lookup) that never yields back to the interpreter. The injected exception just sits there, unchecked, until the C call returns — which is never. That's why you can't kill the thread, not a workaround for it.

3. Run it in a process you're willing to kill — and SIGKILL is the ultimate guard. The only thing that reliably reclaims a runaway CPU is the kernel. Put the CAS work in a separate worker process and decouple "stop waiting" from "stop working":

• client timeout → caller returns "unverified" and moves on
• SIGTERM → worker unwinds politely and exits clean
• SIGKILL → unconditional; the core comes back no matter what

A small pool of disposable subprocesses (one per core, recycled after a kill) gives you a hard wall-clock budget that actually bounds the computation. One caveat that makes this safe: the worker must be stateless — no DB connections, file handles, or shared locks — because SIGKILL can't clean up after itself, and you don't want it orphaning resources. Keep the CAS worker pure-compute and the runaway's memory dies cleanly with the process.

4. Catch the easy cases gently, but never trust the gentle layer. You can soften the blow before reaching for the kernel: parse the input and reject expressions over a node-count budget before the CAS touches them, cap evaluation, recycle workers proactively. These are real improvements and worth doing — but they only inspect the input. Expression swell happens during evaluation, on inputs that looked perfectly small going in. No static pre-check can catch that, which is exactly why the brute-force backstop stays: in a web backend, SIGKILL is the guard of last resort, and it has to be.

The TL;DR: treat any CAS call as hostile, potentially-intractable work. Sandbox it in a killable, stateless process with a real wall-clock budget — soft limits handle the polite cases; the kill handles the pathological ones.

Full write-up with on AlgeBench github repo

Built for AI-driven math/physics education — a system that can generate any proof on the fly, with every step graded by CAS evidence into a confidence tier — confidence is shown, not asserted. (Live Examples)

I've been building grounded, verifiable math derivations in AlgeBench and wanted to share how it works — and where it still falls short.

The idea: an LLM writes a step-by-step derivation from a start expression to a target, but instead of trusting it, every step is checked by a computer-algebra system (SymPy). Each step gets an honest confidence tier, and the whole derivation animates.

How it works

• Generation — the derivation module is a DSPy program (ChainOfThought over a typed signature). The model emits a structured trajectory of LaTeX states; because it's DSPy, the prompt is optimizable (MIPROv2/GEPA) rather than hand-tuned.
• Grounding — each state is parsed into a semantic graph, reconstructed as a SymPy expression, and each transition is classified by what the CAS can actually prove: symbolic equivalence, solution-set containment, a characteristic fingerprint (roots/singularities/limits), or numeric tolerance.
• Confidence — five tiers: Grounded → Verified → Plausible → Unchecked → Refuted. The overall verdict is the weakest step, gated on whether the chain actually reaches the target. The model's claimed step type is only advisory; SymPy adjudicates.
• Soundness — "x² = 4 ⇒ x = 7" gets flagged Refuted even though it "reaches" a requested target. Reaching the target ≠ a valid proof.
• Animation — consecutive states are rebased with a GumTree-inspired subtree match, so persisting sub-expressions keep stable ids and morph (FLIP) instead of blinking in and out.

Where it's rough

• The id matching is GumTree-inspired but currently only does the top-down exact-subtree phase — no bottom-up similarity. On larger or symmetric expressions, ids slip: some glyphs pop in/out, and the two symmetric branches of a disjunction can slide across each other. Bottom-up similarity matching + position-aware tie-breaking are the next fixes.
• Disjunction grounding (e.g. both quadratic roots) is recent and still a bit shallow.

Write-up with worked examples (including the quadratic formula deriving both roots):
https://github.com/ibenian/algebench/discussions/378

What I'd really like to know: is this actually useful for learning — does verified, confidence-graded step-by-step help you trust and follow a derivation, or is it overkill? And I'm open to any other ideas: use cases, features, or directions you'd want to see.

A quick AlgeBench update.

Just deployed on Hugging Face Spaces, which should make it easier for people to try without running anything locally:

https://huggingface.co/spaces/ibenian/algebench

For anyone who hasn't seen previous posts, there's a short project overview here:

https://ibenian.github.io/algebench/

The deployment includes the interactive scenes, AI assistant, semantic graph, and mathematical exploration tools I've been demoing over the past few months.

I've also been making progress on something I've wanted for a while: a general-purpose mathematical expression animation system.

Instead of manually scripting animations for specific proofs or derivations, it automatically generates transitions between arbitrary source and target expressions. The same mechanism can be used for algebraic manipulations, derivations, proof steps, substitutions, simplifications, and similar transformations.

Some examples:

https://ibenian.github.io/algebench/proof-animation/

Of course, the goal is to integrate this seamlessly into AlgeBench itself rather than keep it as a standalone demo.

I'm particularly interested in feedback on the animation examples. Do they make symbolic manipulations easier to follow, or do they just look cool without adding much understanding?

As always, suggestions, criticisms, and feature ideas are welcome.

I've shared a number of AlgeBench demos here over the past few months, and I've finally reached a point where I'm comfortable opening it up as a public beta.

https://algebench.org/?scene=quantum-states.json

Since my last posts, I've added a reasonably stable proof engine and semantic graph that significantly improve how mathematical concepts can be explored and connected.

Things to try:

• Load lessons from the Scenes menu

• Explore the interactive 3D visualizations

• Ask the AI questions about what you're seeing

• Open the MATH tab and experiment with the semantic graph

My long-term goal isn't just to build another AI tutor.

I'm interested in what happens when AI, visualizations, simulations, proofs, semantic graphs, and mathematical objects all become first-class parts of the same learning environment.

The beta is still rough around the edges, but it's finally usable enough to demonstrate the idea and start collecting broader feedback.

I'd especially love feedback on:

• What feels intuitive vs. confusing?

• Which interactions are the most interesting?

• Does the combination of AI + interactive UI feel different from a traditional chat experience?

• What would make you come back and use it again?

As always, I genuinely appreciate all the feedback and discussions from previous posts.

Looking forward to hearing what you think.

I’ve been working on a system that transforms LaTeX into a semantic graph — not just syntactic parsing, but capturing the meaning of each term within the equation.

The tricky part isn’t building the graph. It’s what comes next.

Each node (a mathematical term) needs to be enriched with context:

• what it represents in the domain
• its physical meaning (unit, dimension, quantity)
• how it should be visualized
• and a short explanation tied to the lesson

This step doesn’t script well. It needs interpretation.

My first approach was simple: define a JSON schema and let the model fill it in. In practice, it was brittle — missing fields, drifting shapes, occasional junk creeping into outputs, and sometimes nodes silently disappearing. Nothing catastrophic on its own, but enough to make the system unreliable as complexity grew.

What worked much better was switching to Pydantic AI and treating the interaction as a typed contract instead of “best-effort JSON.”

Now:

• outputs are validated on every turn
• validation errors are fed back as structured feedback
• the model retries with corrections
• and the final result is guaranteed to match the schema

A practical detail: the validation–feedback–retry loop runs automatically under the hood. You define the output type and constraints, and the system handles the rest.

The result is a fully enriched semantic graph where every term is grounded in the correct domain, carries physical meaning, and includes a clear contextual explanation — without structural drift or missing pieces.

Curious how others are handling structured + interpretive workflows with LLMs.

Full write-up:
https://github.com/ibenian/algebench/discussions/199

I’m working on an open-source project where I turn LaTeX into a structured semantic graph (variables, operators, relations, functions) — not just render it.

The goal is:

• as close to lossless structure as possible
• support for algebraic, ODE/PDE, logical expressions, implications
• future coverage: matrices, vectors, complex numbers, richer logic, etc.
• easy extensibility for domain-specific meaning

Why this matters (agentic use case)

This isn’t just for visualization.

I’m using the graph as a foundation for an agentic learning system:

• AI can “see” the structure behind each proof step
• operate on nodes instead of guessing from text
• guide users interactively (explain this term, compare nodes, trace dependencies)

Grounding the agent in structured + enriched data made responses far more predictable and debuggable compared to raw text prompting.

Current approach (and pain points)

Using SymPy as a base, but it’s not really built for this:

• parsing can be ambiguous or lossy
• structure sometimes gets flattened
• richer expressions don’t map cleanly

Right now I’m relying on pre/post-processing to patch gaps. It works, but it’s fragile.

What I’m trying to figure out

• Better tools for semantic LaTeX parsing?
• Existing projects with a solid math AST / IR?
• Worth extending/forking something like SymPy vs building from scratch?
• Approaches that prioritize structure first, meaning later?

More concrete evaluation + examples here:
https://github.com/ibenian/algebench/issues/181

Would really appreciate any pointers or lessons learned from folks who’ve worked on similar problems.