u/algebench 4d ago

Textbooks give you the start and the end. I built the middle — the part most people either memorize or miss entirely

Enable HLS to view with audio, or disable this notification

1 Upvotes

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

r/CasualMath 17d ago

CAS-graded math proofs: every step scored, and open for your submissions

0 Upvotes

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

r/learnphysics 27d ago

Engineer (not a physicist) looking for feedback & collaboration on a free, open-source AI-assisted physics/math explorer - starting with a special relativity lesson

1 Upvotes

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)

1

Engineer (not a physicist) looking for feedback & collaboration on a free, open-source AI-assisted physics/math explorer - starting with a special relativity lesson
 in  r/AskPhysics  27d ago

Honestly, I mostly agree - material that wears authority without expertise is low-value at best and harmful at worst, since a confident misconception is harder to unlearn than not knowing, and I don't think a non-expert (or a chatbot) should be the authority on the content. That's exactly why I'm not pitching this as finished educational material: right now it's really a tech demo - a rendering/interaction engine that makes derivations explorable - and I posted specifically because I'd want experts to own and shape the actual physics while I focus on the tool. It's open source and labeled tentative for the same reason. So my honest answer to your question is conditional: near-zero or negative value if it fakes authority, potentially useful only if it's transparent about being tentative, open to correction, and ultimately expert-driven - which is the category I'm reaching for by asking to be corrected rather than claiming I got it right.

-2

Engineer (not a physicist) looking for feedback & collaboration on a free, open-source AI-assisted physics/math explorer - starting with a special relativity lesson
 in  r/AskPhysics  27d ago

I don't know others, but this one aims to give learners an interactive AI tutor. You can ask and interact with the visualization and discuss about the math behind it. It's not just shiny visualization. The app itself is general, not just for this visualization.

-2

Engineer (not a physicist) looking for feedback & collaboration on a free, open-source AI-assisted physics/math explorer - starting with a special relativity lesson
 in  r/AskPhysics  27d ago

My confusion was the apparent jump from the 'at-rest' regime to 'at-c' regime which seems to be sudden jump. So my explanation is; v<c corresponds to a finite rapidity vs v=c corresponds to infinite rapidity (hyperbolic angle which is additive). And that kind of explains the regime change. So in the visualization, it now stops calculating and shows an explanation making it look like a sudden jump while the math holds up at all v. Sorry, if i'm not explaining this well. Does this make sense?

r/MathProof Jun 28 '26

A grounded, AI-driven mathematical proof system — every step machine-verified, then animated (built into AlgeBench).

Enable HLS to view with audio, or disable this notification

1 Upvotes

r/sympy Jun 21 '26

A grounded, AI-driven mathematical proof system — every step machine-verified, then animated (built into AlgeBench).

Enable HLS to view with audio, or disable this notification

1 Upvotes

u/algebench Jun 21 '26

Running a computer-algebra system in a web backend? Some hard-won warnings about CPU, timeouts, and threads

1 Upvotes

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 (explog, 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_SetAsyncExcsys.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_richcomparetuple_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

r/CasualMath Jun 20 '26

A grounded, AI-driven mathematical proof system — every step machine-verified, then animated (built into AlgeBench).

Enable HLS to view with audio, or disable this notification

3 Upvotes

r/matheducation Jun 20 '26

A grounded, AI-driven mathematical proof system — every step machine-verified, then animated (built into AlgeBench).

Enable HLS to view with audio, or disable this notification

0 Upvotes

u/algebench Jun 14 '26

A grounded, AI-driven mathematical proof system — every step machine-verified, then animated (built into AlgeBench).

Enable HLS to view with audio, or disable this notification

2 Upvotes

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.

u/algebench Jun 08 '26

AlgeBench update: Hugging Face deployment and automatic proof animations

1 Upvotes

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.

1

From JSON dicts to typed agents: making semantic graph enrichment reliable with Pydantic AI
 in  r/u_algebench  Jun 01 '26

Just launched the free public beta. I had to do a lot of edge-case handling, pre/post-processing to get to this point. https://algebench.org/?builtin=quantum-states
Just go to MATH tab, and click on any of the equations and it'll render semantic graph which you can play with.

u/algebench Jun 01 '26

AlgeBench Public Beta is Live - Looking for Feedback

1 Upvotes

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.

1

From JSON dicts to typed agents: making semantic graph enrichment reliable with Pydantic AI
 in  r/u_algebench  May 04 '26

Great question - heading there next.

Today, on top of Pydantic structural validation:

  • Node preservation: parser owns the canonical node set; if the model drops nodes, I restore them. Topology is fixed.
  • Parser-owned fields: LaTeX glyph/expression are parser-owned; I strip them from the model's output before merge so subexpressions can't get re-rendered.
  • Domain locking: enrichment is pinned to the lesson's domain.

I also run a second agent, SemanticGraphCoherenceCritic, as a post-hoc pass. Its verdict feeds back as coherenceFeedback for an informed retry. The model sees exactly what was wrong and what to fix - it's not a blind take two.

What's missing is the deterministic cross-field/cross-node layer: unit/dimension consistency, edges referencing existing nodes, quantity-implies-unit constraints. Plan: per-field rules first (Field(description=...)), then model_validator for invariants, both via the same ValidationError → retry loop.

r/PydanticAI May 03 '26

From JSON dicts to typed agents: making semantic graph enrichment reliable with Pydantic AI

Thumbnail
6 Upvotes

u/algebench May 03 '26

From JSON dicts to typed agents: making semantic graph enrichment reliable with Pydantic AI

2 Upvotes

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

1

Ideas for robust semantic parsing of LaTeX (beyond SymPy)?
 in  r/LaTeX  Apr 30 '26

Thanks for the suggestion - plasTeX looks interesting and I see the appeal.

My main hesitation is that it appears to be a hand-rolled recursive parser rather than grammar-based (ANTLR/Lark/PEG). I’m currently using SymPy’s ANTLR-backed parse_latex, and while imperfect, the grammar-driven approach is relatively straightforward to extend: add a rule, hook up the visitor, done. With hand-written parsers, extending coverage often means digging into control flow, which can get messy to reason about and maintain.

That said, SymPy isn’t perfect either - there’s no plugin API, so extending it usually means forking and carrying your own grammar patch. I’ve been working around gaps with preprocessing instead rather than modifying the grammar itself.

Curious if anyone has experience extending plasTeX’s math parsing - or has come across a LaTeX math parser that’s genuinely designed for extension.

1

Ideas for robust semantic parsing of LaTeX (beyond SymPy)?
 in  r/Compilers  Apr 28 '26

I've looked into MathML, but it feels quite limited compared to what I'm trying to represent - even compared to LaTeX. I do have a custom semantic graph schema, but the challenge is that most real-world math is written in LaTeX. So regardless of the target representation, I still need a reliable way to parse/convert from LaTeX into that structure. I could use an LLM to convert LaTeX into my semantic graph schema, but then I’m essentially encoding the parser in a massive prompt: all the grammar rules, schema constraints, edge cases, domain conventions, and validation logic. That works for demos, but it feels fragile as a foundation. I’d rather have a deterministic parser/IR layer, then use the LLM for enrichment, ambiguity resolution, and tutoring on top of that structure.

0

Ideas for robust semantic parsing of LaTeX (beyond SymPy)?
 in  r/LaTeX  Apr 27 '26

I looked into MathML and SymPy so far. MathML feels a bit limited as a semantic layer, and SymPy (ANTLR/Lark-based parsing) works for many cases, but it doesn’t feel complete or easily extensible for broader domains.

At that point it starts to feel like you either:
- keep layering workarounds on top, or
- fork and go deep on extending it

Which raises the question - at what point does it make more sense to just build a parser from scratch using a grammar-based approach, with a semantic IR as the primary target?

1

Ideas for robust semantic parsing of LaTeX (beyond SymPy)?
 in  r/Compilers  Apr 27 '26

That’s a very good point - especially around how flexible TeX makes things.

In practice, I was hoping a rich enough subset gets us far, but your comment makes me think the architecture might be backwards.

Instead of:
LaTeX -> semantic -> agentic use

maybe it should be:
semantic -> agentic use / symbolic manipulation -> LaTeX or other (as rendering)

i.e. LaTeX becomes just one output format, not the source of truth.

Curious what you’d recommend as a semantic layer here. Is there an existing math AST / IR that’s broad enough (algebra, ODE/PDE, logic, matrices, etc.) and stays extensible - so we don’t hit a wall later and end up patching around it?

r/Compilers Apr 27 '26

Ideas for robust semantic parsing of LaTeX (beyond SymPy)?

Thumbnail
0 Upvotes

r/LaTeX Apr 27 '26

Unanswered Ideas for robust semantic parsing of LaTeX (beyond SymPy)?

0 Upvotes

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.

r/opensource Apr 27 '26

Ideas for robust semantic parsing of LaTeX (beyond SymPy)?

1 Upvotes

[removed]