SAMOSA

Step Auditor for Matrix Operations, Stochastics & Algebra

Check every step of your derivation. Exactly. In your browser.

→ Live demo · Report a bug · Request a feature

     ∇
    ╱ ╲
   ╱   ╲      "A ∇ is just a samosa with filling."
  ╱_____╲

SAMOSA is a linter for math derivations. Paste a LaTeX align block, a
Markdown note, or the answer a language model gave you, and every row gets
one of these:

• ✓ holds, with the sizes it was tested at, the number of trials, the
  primes, and the probability that a wrong step slipped through
• ✗ wrong, with a small counterexample and a fix
• ⊘ shape error, with the sizes that do not fit
• ? not checked, with the reason

There is no language model in the verdict path. There is arithmetic, a finite
field, and a probability bound.

Why SAMOSA?

A derivation is a chain of small steps, and the errors are small too. A
transpose in the wrong order. A dropped + KQKᵀ. A factor of two from
treating a non-symmetric matrix as symmetric. A gradient in the wrong layout.

The step that nobody checks is the one that says "after some algebraic
manipulation, we may obtain ...".

SAMOSA started with exactly that step. The Kalman measurement update, as it
is usually written, says

after some algebraic manipulation we may obtain K = Σ̄Cᵀ(CΣ̄Cᵀ + Q)⁻¹

and that is the one line in the notes that no one ever verified. SAMOSA
checks it, exactly, and it also finds the two ways you can get it wrong.

What it does

See it work

Nineteen seconds. The line everybody writes and nobody checks, and what
happens when a machine reads it.

A transposed product. The squiggle, the counterexample, and the fix that
takes one keystroke.

The Kalman update, with the missing noise term. The row everybody writes
from memory, and the term that is not there.

A gradient in the wrong layout. The numerator layout is a transpose away
from the right answer, and SAMOSA says so.

Quick start

# the web app
npx samosa-math check paper.tex

# the CLI
npx samosa-math check paper.tex --format sarif

# the MCP server, for Claude Code, Codex or Cursor
claude mcp add samosa -- npx -y -p samosa-math samosa-mcp

The declarations go in a comment, in the compact syntax:

% samosa: x_t, \bar\mu_t: n; z_t: m; C_t: m×n; Q_t: spd m; \bar\Sigma_t: spd n

The example

\begin{align*}
J_t &:= \tfrac12 (z_t - C_t x_t)^\top Q_t^{-1} (z_t - C_t x_t) + \tfrac12 (x_t - \bar\mu_t)^\top \bar\Sigma_t^{-1} (x_t - \bar\mu_t) \\
\frac{\partial J_t}{\partial x_t} &= -C_t^\top Q_t^{-1}(z_t - C_t x_t) + \bar\Sigma_t^{-1}(x_t - \bar\mu_t) \\
\frac{\partial^2 J_t}{\partial x_t^2} &= C_t^\top Q_t^{-1} C_t + \bar\Sigma_t^{-1} \\
\Sigma_t &:= \left(C_t^\top Q_t^{-1} C_t + \bar\Sigma_t^{-1}\right)^{-1} \\
\frac{\partial J_t}{\partial x_t} = 0 &\implies x_t = \bar\mu_t + \Sigma_t C_t^\top Q_t^{-1}(z_t - C_t \bar\mu_t) \\
K_t &:= \Sigma_t C_t^\top Q_t^{-1} \\
K_t &= \bar\Sigma_t C_t^\top \left(C_t \bar\Sigma_t C_t^\top + Q_t\right)^{-1} \\
\Sigma_t &= (I - K_t C_t)\, \bar\Sigma_t
\end{align*}

SAMOSA reports every row as holding, at the sizes (3,2), (2,3) and (4,3),
with three trials in each of two primes, and a false checkmark bound below
10⁻⁴⁶ per size.

Now change one thing. Put Q_t^{-1} inside the inverse on the push-through
row, and SAMOSA says the two sides are not equal, gives you the smallest
counterexample, and tells you the term you are missing.

How much of a real paper it reads

Measured, not guessed. The display math of 36 recent papers from cs.LG,
cs.RO and stat.ML, 1416 rows. 197 rows make no claim and are excluded; of
the 1219 claim rows:

That is 21.5% of all 1416 display rows. The first version of this table
parsed only the first expression of each row and reported 86.8% and 50.0%.
It was lenient, and this one replaces it. What stops the rest is a cases
block inside a probability, a script on something that is not a symbol, a
set the parser cannot close, and the macros the authors define themselves.
The method, the correction and the full list of what stops the rest are in
docs/COVERAGE.md.

And the Cookbook: 48 identities in matrix algebra, calculus and stochastics,
with the mistakes the catalog can make of them.

The plan's gate asks for 95% of the bugs caught. The cookbook is at 74.8%,
and every miss is a step the engine says it cannot decide, never one it
calls right. The method, the misses and the bugs the corpus found are in
docs/COOKBOOK.md.

What it cannot do

Being straight about the edges is part of the product:

• It does not prove theorems. It checks steps.
• It does not check inequalities (≤), limits, or series. Those come back
  as ? with a reason.
• It does not check the prose around the equations.
• It does not understand every notation. When it does not, it says so, and
  tells you which declaration would help.
• It does not know your paper is right. It knows that one row is not.

The menu

Sixteen derivations that people actually write, each with a correct version
and a planted bug, in the app and in the golden test suite: Woodbury,
Sherman-Morrison, the matrix determinant lemma, the trace identities, the
Kalman update, the Joseph form, least squares, ridge regression, logistic
regression, the softmax cross entropy, a two layer network, the variance of
a Gaussian, the expectation of a quadratic form, the KL of two Gaussians,
the Riccati recursion, and rotations and the cross product.

The install

How it works

The short version: SAMOSA never rewrites symbols. It samples the objects
your declarations describe, with the structure they ask for, and evaluates
both sides of every step on the same instance. Non-commutativity, structure
and shape all come for free.

The long version, with the probability bounds and the two honest caveats,
is in docs/HOW_IT_WORKS.md.

The notation

docs/NOTATION.md has the full list: what a superscript
means, how a symbol is named, what the relations do, and the declaration
syntax in both the LaTeX and the compact form.

Privacy

Your derivation never leaves your machine. The engine is a Web Worker in
the tab, a share link keeps the derivation in the URL fragment, and the CLI
and the MCP server make no network requests at all. See
docs/PRIVACY.md.

Development

pnpm install
pnpm dev            # the site and the app
pnpm test           # the unit tests
pnpm test:e2e       # the browser tests
pnpm lint
pnpm build          # the site
pnpm build:pkg      # the npm package

The engine lives in src/core and imports nothing from the DOM or from
Node, so the same code runs in the browser, in the CLI and in the MCP
server. The rules it lives by: no model in the verdict path, never a
checkmark without a guarantee, and nothing that leaves the machine.

Contributing

Issues and pull requests are welcome. The best ones come with a derivation
that SAMOSA gets wrong: a notation it cannot read, a step it should catch
and does not, or a false checkmark. Those are the bugs that matter.