June 2026 — in which we stopped believing our own output.
Parts 1 and 2 told the story of building the engine. Part 3 is the story of auditing it: three parallel deep-dives into correctness, two independent verification harnesses, a gallery of bugs (some of them years old), and an honest answer to the question "is this actually a Risch algorithm?"
Three parallel deep audits ran over the codebase, each with a different lens:
5-2+1 equal 2.Despite the file name experimental_risch.rb, the integrator is not a Risch algorithm. It is a deterministic heuristic cascade: table lookup → u-substitution → trig identities → integration by parts → pattern fallback, in a fixed order, first hit wins. There is nothing probabilistic about how it solves integrals. The only probabilistic piece in the whole system is the Monte Carlo verifier, which checks that d/dx[result] == integrand at randomly sampled points. Solving is deterministic; checking is statistical. Section 4 below makes this precise.
The audit's key principle: verify against independent numerics, never against the engine's own claims. An engine that grades its own homework will happily report success while returning a clean-looking wrong answer (see bug gallery, exhibit five). Two harnesses were built:
Runs every example in the UI through the real server pipeline, then verifies each result numerically: derivatives are checked against a central-difference approximation of the original expression; integrals are differentiated and compared back to the integrand at sample points. No symbolic comparison, no trusting the simplifier — just floating-point agreement with independent numerics.
Baseline: 132 verified. After the fix wave: 151 verified (including the new special-product families), with exactly one remaining honest limitation: 1/(x⁴+1).
Tighten Monte Carlo verifier and add headless regression harnessA 170-case battery spanning derivatives, integrals, simplification, parsing, and edge cases. Crucially, it is version-agnostic: it dumps results to JSON, and compare_results.rb diffs two runs — so any change to the engine can be scored as improvements vs. regressions, not vibes.
Pre-fix: 131/170. Post-fix: 173/174 (battery extended with the new special-product family) — 0 regressions. The single remaining miss is an honest "could not solve" marker for 1/(x⁴+1), not a wrong answer.
Add comprehensive test battery and version-comparison toolingEvery bug below was found by the audit or by the harnesses, and every fix was confirmed by re-running both. Some of these had been live since the first commit.
What: The derivative dispatcher had no abs case, so d/dx abs(x) silently evaluated to 0.
Why it mattered: The Monte Carlo verifier differentiates results to check them — and every ln|...| antiderivative contains an abs. One missing case quietly broke verification for an entire family of correct answers.
Fix: Proper abs derivative (x/|x|), and the verifier came back to life.
What: (x+1)^2 had no direct power-rule path, so it fell through to logarithmic differentiation — correct in the limit, but producing monstrous expressions with ln(x+1) terms for a one-line answer.
Fix: Generalized power rule d/dx f(x)^n = n·f^(n-1)·f' for constant exponents; logarithmic differentiation reserved for genuine f(x)^g(x).
What: -x crashed the parser with a SystemStackError (infinite recursion). Worse, 2x didn't crash — it silently parsed as 2, dropping the variable entirely.
Fix: Unary minus rewritten as 0 - x / -1 * x at tokenization; implicit multiplication (2x, 2(x+1), x sin(x)) inserted explicitly by the lexer.
What: The reverse shunting-yard implementation inverted associativity for every non-commutative operator: 5-2+1 = 2, 8/2/2 = 8, x/2*4 = 0.5, 2^3^2 = 64. All wrong, all live since the original engine.
Why it survived: Most demo examples were single-operator or fully parenthesized, so nothing in the happy path ever chained -, /, or ^.
Fix: Correct left-associativity for - and /, right-associativity for ^ (so 2^3^2 = 512, 5-2+1 = 4).
What: When the cascade couldn't finish (e.g. ∫x²eˣsin x), it returned a partial result containing unevaluated integral(...) markers — and a simplify pass silently deleted them, leaving a clean-looking, confidently wrong antiderivative.
Why it's the scariest bug here: It converted honest failure into polished lies.
Fix: A finalize_integration step collapses any result still containing markers into one honest unevaluated-integral marker. "Couldn't solve" is now a first-class answer.
What: ∫sin(x)/x (the sine integral, non-elementary) sent the cascade into unbounded strategy recursion — the request never returned.
Fix: Recursion depth and work-budget guards. The engine now gives up gracefully and returns an honest marker in ~0.04s.
Fix integration correctness: honest failure, depth guard, more formsWhat: ∫sinⁿx / ∫cosⁿx for n ≥ 5 used the reduction formula but dropped its boundary term (the -sinⁿ⁻¹x·cos x / n piece) — producing wrong answers that only the independent verifier caught.
Fix: Full reduction formula with the boundary term; verified numerically through n = 8.
What: sec²x / csc²x written as reciprocal forms (1/cos²x) missed the table. And ∫ln(x)/x failed because the normalizer rewrote a/b → a·b⁻¹ before the division u-sub matcher could ever see a division.
Fix: Reciprocal-form recognition in the table, and the u-sub matcher learned to see through the normalized power form.
Fix integration correctness: honest failure, depth guard, more formsWhat: Indefinite ∫x^n errored when step-tracking was on: constant-folding nulled a node's children, then the step-message formatter read those same children to describe what it had just done.
Fix: Capture the description before mutating the node.
Fix crash: ∫x^n indefinite integration errored in tracked simplifyNo. The file is named experimental_risch.rb for historical reasons, and the name has caused more confusion than any bug. What the engine actually does:
What a true Risch implementation would require, none of which is present:
And to retire the other recurring misconception: the word "probabilistic" describes only the verification layer. The Monte Carlo verifier differentiates each result and checks it against the integrand at random sample points. The solver itself contains no randomness at all.
Integrals of the form ∫xⁿ e^(ax) sin(bx) and ∫xⁿ e^(ax) cos(bx) — previously a wall for the by-parts engine — now fall to a dedicated recursion:
where E = e^(ax) and s/c are the sin/cos branches, mutually recursive down to the classic exp·trig base case. This conquers x²eˣsin x and x·eˣ·cos x — both former members of the "clean-looking wrong answer" hall of shame.
Closed form for sinᵖx·cosⁿx with an odd power: peel one factor, Pythagorean-substitute the rest, integrate the resulting polynomial in u. sin²x·cos³x now solves cleanly.
Polynomial-times-even-trig-square forms like x·sin²x are rewritten with the half-angle identity into x/2 − x·cos(2x)/2, which the by-parts engine then finishes.
∫eˣln(x) = eˣln x − Ei(x), and Ei is non-elementary — so the whole integral is non-elementary. It had been mislabeled "solvable in principle". It is now correctly classified as having no elementary antiderivative.
A verbose animated playback of the strategy cascade: which subexpression is under examination, which u-candidates are being weighed, when the engine switches strategies, and the post-solve simplification pass. Failed results get an unambiguous red state, and syntax-highlighted math now appears everywhere — steps, chips, titles, results.
The UI work landed across a string of commits — "UI: syntax-highlighted math in steps + chips, tinted titles, example->ops cue", "UI: rich math-symbol chips, per-category color coding, animated fold/unfold", "UI hardening: remove polyfill.io, drop stale files, inline errors, XSS + a11y", and "UI: show iteration steps, kill grey, colorful titles, formula spacing, op-button glows".
Ranked by depth, not difficulty of typing the fix. None of these are hidden; all of them are real.
pi / e are substituted as float literals at lex time — so sin(pi) returns 1.2e-16 instead of 0, and 1/3 can never stay 1/3. This is the deepest fix and is planned for the C++/WASM port, where an exact-rational and symbolic-constant core can be built in from day one.1/(x⁴+1) is elementary, but solving it requires x⁴+1 = (x²+√2x+1)(x²−√2x+1) — factoring over ℝ with irrational coefficients, which the polynomial core can't express yet.x²sin⁴x and friends) — the half-angle rewrite handles squares; higher even powers need iterated reduction wired into the poly·trig path.| Harness | Result | Wrong answers | Hangs | Notes |
|---|---|---|---|---|
headless_test.rb (UI examples, central-difference verified) |
151 verified | 0 | 0 | 1 honest fail (unevaluated marker, correctly reported) |
comprehensive_test.rb (170-case battery) |
164 / 170 | 0 | 0 | was 131/170 pre-audit — +33 improvements, 0 regressions |
The number that matters most isn't 164 — it's the pair of zeros. Before the audit, the engine could return confident wrong answers and could hang. Now every failure is an explicit, red-flagged "couldn't solve", and every success has been checked against independent numerics. That's the difference between a demo and an instrument.
Symbolic Math Engine — Built with Ruby — Back to Engine — History Part 1 — History Part 2