Goal: Math OS — a ten-year vision for AngouriMath as an open mathematical reasoning platform

> **What this issue is.** A long-term technical vision, written to be argued with. It sets a
> direction for the next decade and a dependency order for getting there. It is not a release plan,
> it is not a commitment of anyone's time, and the version numbers below are *capability tiers*,
> not shipping dates.
>
> **What this issue is not.** A rewrite proposal. Nothing here requires starting over — the opposite,
> in fact: the argument is that AngouriMath already has the parts nobody else in .NET has, and that
> the work is to make them into a platform rather than a set of endpoints. [#497](https://github.com/asc-community/AngouriMath/issues/497)
> proposed evolution by rewrite and stalled; this proposes evolution by layering.
>
> **How to use it.** Comment to disagree. Open issues for the pieces you want to own, link them here,
> and check them off. Anything in *How contributors can help* is fair game today, without waiting for
> a single line of this to be ratified.
>
> **Edited 2026-08-07** to fold in review from this thread: a packaging split so the common case does
> not carry edge-case machinery, benchmarking as a standing condition rather than a roadmap item, and
> trimming/NativeAOT-safety as a structural constraint on extensibility. See
> *Packaging, and what must never regress*, and items 78–80.
>
> **Edited 2026-08-23** to reconcile the checklist with what the repository actually contains, rather
> than with what the issues say. Completed items are struck through with the pull request that
> delivered them; partial ones keep their text and gain a **Remaining** line naming the half that is
> missing, because "partial" without saying which half is worth nothing. Nothing is deleted — a
> finished item is still the record of a decision. Where the audit contradicts a closed issue or an
> open one, the code won; three closed issues do not match their code and two open ones are done.
> See *Where the tiers stand* below.

---

# Vision

## Mathematical software is a pile of isolated algorithms

Look at what a computer algebra system offers a caller today, ours included. A handful of top-level
entry points — `Solve`, `Integrate`, `Limit`, `Simplify`, `Differentiate` — each a procedure you
invoke and hope. Every one is a self-contained tower of knowledge, and every one of those towers is
sealed.

Three things follow from that shape, and all three limit us.

**Knowledge does not accumulate.** Our limit code knows that a difference of large terms should be
expanded before comparison. Our solver knows that a substitution can linearise an equation. Our
integrator knows which substitutions rationalise a radical. These are the *same kind* of fact — "this
transformation is worth trying on an expression of this shape, for this reason" — and there is no
place to put such a fact where all three can use it. So each is re-discovered, re-encoded, and
re-tuned inside its own method. Adding the Nth algorithm costs about as much as adding the first.
That is the defining property of a library and it is the thing to escape: we want a system where
algorithm N+1 is *cheaper* than algorithm N, because N built infrastructure that N+1 inherits.

**Answers are not inspectable.** `"x^2 - 4 = 0".Solve("x")` returns `{-2, 2}` and there is nothing
else to ask. Not *why*, not *by what route*, not *under which assumptions*, not *what was tried and
failed*. This is not a missing feature; it is a missing data structure. A derivation was constructed
inside the call and thrown away at the return statement. Everything valuable that could be built on
top of an answer — teaching, hint generation, verification, error messages that say what is actually
blocking, a machine deciding whether to trust the result — needs that discarded object and cannot be
retrofitted from a string.

**Failure is uninformative.** When we cannot do something, the caller gets an unevaluated node. That
is honest (and our discipline about it is one of the better things about this codebase — see
[AGENTS.md](https://github.com/asc-community/AngouriMath/blob/master/AGENTS.md): *unevaluated* means
"I could not settle this", `NaN` means "this does not exist", and confusing them is a wrong answer).
But honest and useful are different bars. "I could not settle this" is a far weaker statement than
"I reduced this to needing the factorisation of a degree-6 multivariate polynomial, which I cannot
do", and only the second tells a contributor what to build, a caller what to try instead, or a
planner where to search next.

None of this is a criticism of the algorithms. Gruntz for limits, Risch for integration, Gröbner for
systems — these are deep, correct, hard-won things, and any serious system needs them. The claim is
narrower and, I think, harder to argue with: **the interface we wrap them in throws away most of what
they know**, and that interface is the ceiling on everything built above.

## What "Math OS" means

Not a user interface. Not a Mathematica clone. Not, emphatically, a new language.

An operating system, in the sense that matters: a layered platform that owns the representations and
the scheduling, so that everything above it composes and everything below it is replaceable. The
useful parts of the analogy:

| OS concept | Math OS |
|---|---|
| kernel object model | the immutable expression tree, with domains and provenance |
| system calls | transformations with stated contracts and stated assumptions |
| scheduler | a strategy engine that decides what to try next, under a budget |
| filesystem | a knowledge graph of objects, theorems and their prerequisites |
| device drivers | domain packages (geometry, statistics, number theory) behind one interface |
| shell | natural-language and agent interfaces, on top, replaceable, not privileged |
| syslog | derivations — every answer carries how it was reached |

The shift the analogy is really pointing at is in how you *ask*. Today:

```csharp
var roots = equation.Solve("x"); // call a procedure, get a value or a shrug
```

The platform version is: *here is a goal; here is what is known; here is my budget; find a route and
show me the route.* The caller stops naming the algorithm. The system chooses, explains, and reports
honestly what it could not do — which means new algorithms become available to every existing caller
the moment they are registered, rather than when every call site is rewritten.

That is not a UI change. It requires the layers to exist: rules that are data rather than code, costs
that are comparable across domains, facts that are queryable rather than compiled in, derivations that
are objects, and failure that is structured. Those are the roadmap.

## Why AngouriMath is the right foundation

Not sentiment — six specific properties, most of which are unusual and expensive to acquire later.

**The tree is immutable and structurally comparable.** `Entity` is a sealed-or-abstract immutable
hierarchy with structural equality and hashing. Every rewrite system worth having needs exactly this:
you cannot memoise, share, hash-cons, deduplicate, or safely explore a search tree in parallel over
mutable nodes. Most projects discover this at year five and cannot fix it. Ours was designed that way
(see [`coding_rules.md`](https://github.com/asc-community/AngouriMath/blob/master/Sources/AngouriMath/Docs/Contributing/coding_rules.md)),
and it means the expensive precondition for the whole roadmap is already paid for.

**One tree spans continuous, discrete, boolean, set-theoretic and matrix mathematics.** Look at
`Core/Entity/{Continuous,Discrete,Omni}`: numbers, functions, statements, sets, `Piecewise`,
`ConditionalSet`, `Provided`, matrices — all one algebra of nodes. That is why `Solve` can return a
set, why a solution can carry a condition, and why an inequality is not a separate universe. Systems
that bolted logic on later cannot express "the solution is this, provided that" as a value. We can,
today. A reasoning platform lives or dies on being able to say things like that.

**Symbolic and numeric are the same object.** `Functions/Compilation/{IntoLinq,IntoFE}` compiles an
`Entity` to a delegate. A reasoning system needs numerics constantly, and not as a separate library:
to sanity-check a candidate identity, to pick a branch, to estimate before proving, to fall back
honestly when no closed form exists. Having compilation in the kernel makes the numeric layer of v6.0
an extension rather than an integration project.

**The printed form is contractually a lie-free channel.** Parsing what `Stringize` prints gives back
the expression printed — enforced by `StringizeRoundTripTest`, with the grammar in
[`AngouriMath.g`](https://github.com/asc-community/AngouriMath/blob/master/Sources/AngouriMath/Core/Antlr/AngouriMath.g)
and the accepted syntax written down in
[`Syntax.md`](https://github.com/asc-community/AngouriMath/blob/master/Sources/AngouriMath/Docs/Usage/Syntax.md).
Machine-to-machine exchange, agent tool calls, corpora, caches and cross-system comparison all rest on
that property. Where it is missing you get a system whose output cannot be fed back into it, which
quietly poisons every dataset built from it.

*Kept honest by measurement, because this paragraph is the one most worth it.* Twice in one week the
contract was found broken in the system this paragraph praises. Until
[#1009](https://github.com/asc-community/AngouriMath/pull/1009) it failed for six operators in a way
that moved the *value*, not merely the shape: `false implies (true implies false)` printed text that
read back as `True`. And until [#1047](https://github.com/asc-community/AngouriMath/pull/1047) it held
for the tree and **not** for everything a node carries — `Stringize` printed no node's `Codomain`, so
`domain(x, ZZ)` printed as `x`, read back with codomain `Any`, and
`e == MathS.FromString(e.Stringize())` was `False`
([#1022](https://github.com/asc-community/AngouriMath/issues/1022)). The parser had accepted
`domain(expr, SET)` the whole time; only the printing half was missing. Both are now fixed and both
are gated by tests.

What is left is smaller and is the grammar's limit rather than the printer's
([#1048](https://github.com/asc-community/AngouriMath/issues/1048)): `Any` has no spelling, so a node
*widened* to it from a narrower default still prints as though it had not been —
`Abs(x).WithCodomain(Any)` prints `abs(x)` and reads back `Real`. That waits on
[#996](https://github.com/asc-community/AngouriMath/issues/996) deciding whether the universal set
deserves a name. The lesson is the one the two fixes share: the round-trip test has to be a **gate**
rather than a belief, and it has to be reflected over every node type rather than hand-listed, which
is what caught both.

**We already refuse to guess.** *Right answer > no answer > slow answer > wrong answer* is written down
and enforced. This looks like a style rule and is actually the load-bearing precondition for
everything in v4.0 and above: **you can plan over a system whose "I don't know" is trustworthy, and you
cannot plan over one that guesses.** A search that treats a confident wrong answer as a solved subgoal
does not degrade gracefully — it produces confident wrong proofs. Very few systems have this property
culturally. We do, and it is worth naming as an asset rather than a constraint.

**The substrate is a platform substrate.** MIT-licensed, cross-platform .NET, with F#, Jupyter
(`AngouriMath.Interactive`), C++ and terminal front-ends already in-tree, AOT on the roadmap, and a
`ToSympy` bridge for cross-checking. Anything built here is embeddable in an IDE, a game engine, a
CAD tool, a teaching app, a CI check or an agent's toolchain without a licence conversation.

And one honest advantage: **we are still small enough to change shape.** The 2.0 paper
([#497](https://github.com/asc-community/AngouriMath/issues/497)) named the real defect — *"one may
find it inconsistent in a lot of places in API, behaviour, and internal structure of code"* — and
proposed a rewrite. The rewrite did not happen, which is the usual fate of rewrites. But the diagnosis
was right, and there is a better cure than starting over: make consistency **mechanically checkable**
rather than aspirational. A rule table you can enumerate, a cost model you can compare against, a
corpus that reports *wrong / error / timeout* counts, a derivation you can replay. Every layer below
turns "we try to be consistent" into something a test can fail on.

---

# Design Principles

Eight principles. Each is stated, justified, and given a **test** — because a principle you cannot
fail a PR against is decoration.

### 1. Composable

Capabilities are values, not entry points. A rewrite rule, a strategy, a cost model, a domain of
knowledge — each is an object you can pass around, combine, restrict, and inspect. Solvers are built
*out of* pieces rather than *alongside* them.

*Test:* can a contributor add a working solver for a new equation class without editing the kernel,
and can they express it as a composition of existing tactics plus their own new one?

### 2. Immutable

`Entity` never mutates. Transformations return new trees. State that a search needs — visited sets,
caches, budgets — lives in explicit context objects, not in the tree and not in statics.

*Test:* any node can be shared across threads and search branches with no copying and no locking.
This is also what makes cancellation and timeouts ([#373](https://github.com/asc-community/AngouriMath/issues/373))
tractable rather than dangerous.

### 3. Deterministic

Same input, same settings, same version, same answer — every time, on every platform, in every
thread count. Rule application order is *defined*, not incidental. No dependence on hash iteration
order, dictionary enumeration, reflection order, or wall-clock timing.

*Test:* a golden corpus reproduces byte-identically across OSes and across single- vs multi-threaded
runs. Where a deliberate timeout makes an answer time-dependent, that must be visible in the result,
not silently swallowed. Non-determinism is the bug that makes every other bug unreproducible.

### 4. Explainable

Every answer can produce the derivation that reached it: the steps, the rules applied, the assumptions
used, and what was tried and abandoned. "Because" is part of the return value, available on request,
not a debug log or a build flag.

*Test:* for any answer the system can emit a derivation that a third party can replay step by step and
independently check. [#273](https://github.com/asc-community/AngouriMath/issues/273) and
[#28](https://github.com/asc-community/AngouriMath/issues/28) are the first two steps of this and have
been open for years — they are infrastructure, not features.

### 5. Extensible

New mathematics arrives as packages, not as kernel patches. Nodes, rules, tactics, theorems and
notation are all registrable. The kernel must not need to know the names of the domains built on it.
([#321](https://github.com/asc-community/AngouriMath/issues/321),
[#338](https://github.com/asc-community/AngouriMath/issues/338),
[#495](https://github.com/asc-community/AngouriMath/issues/495) all point this way.)

*Test:* a third-party NuGet package adds a genuinely new mathematical domain with no fork and no
kernel change — and if it is uninstalled, everything else still builds and behaves identically.

*Constraint, and it is a sharp one:* **extensibility must not be bought with runtime reflection.**
Assembly scanning and `Activator`-style construction break assembly trimming and NativeAOT — which
are exactly the deployment modes the embedded, mobile and game-engine cases need, and which
[#363](https://github.com/asc-community/AngouriMath/issues/363) and
[#552](https://github.com/asc-community/AngouriMath/issues/552) already ask for. This collides
head-on with [#338](https://github.com/asc-community/AngouriMath/issues/338) (looking types up in the
assembly to parse them from a string) and with any plugin loader in v9.0, and the collision should be
resolved deliberately rather than discovered at publish time: prefer **source generators and explicit
registration** over runtime type lookup, and where a reflective path is genuinely unavoidable, keep it
opt-in, off the hot path, annotated for the trimmer, and covered by a test that publishes trimmed and
runs. (Raised by @Happypig375 in this thread.)

### 6. AI-friendly

Every artefact has a machine-readable form and a stable identity: nodes, rules, derivation steps,
theorems, failures. There is an API that takes goals rather than method calls. Serialization is
first-class ([#323](https://github.com/asc-community/AngouriMath/issues/323)).

*Test:* an agent can, using only documented interfaces, pose a problem, receive a structured
derivation or a structured explanation of failure, and verify the result without human help. The
division of labour to design for: **language models are strong proposers and weak verifiers; the
platform must be the verifier.** Every design choice that makes verification cheap is worth more than
one that makes generation slightly better.

### 7. Formalizable

Every transformation carries a justification precise enough that a proof assistant could in principle
check it — or is explicitly labelled as not carrying one. Three tiers, never blurred:
**sound**, **sound under stated assumptions** (domains, `Provided`, branch cut choices), and
**heuristic** (worth trying, proves nothing).

*Test:* the system can answer "which steps in this derivation are unconditionally valid?" and the
answer is derived from the rules, not from a comment. This is what makes v7.0 possible at all; if the
justification is not captured when the rule fires, no later layer can reconstruct it.

### 8. Domain-independent

The kernel knows trees, rules, costs, goals and proofs. It does not know trigonometry. Trigonometric
identities are a package that ships with us and is not privileged by us.

*Test:* the dependency graph has no arrow from the kernel to any specific area of mathematics. If you
deleted the trig rules, the build would succeed and only trig would get worse.

**One meta-principle above all eight.** From
[AGENTS.md](https://github.com/asc-community/AngouriMath/blob/master/AGENTS.md), and it outranks
everything on this list: *right answer > no answer > slow answer > wrong answer.* No layer of this
architecture is permitted to trade correctness for capability. A planner that guesses, an LLM
interface that fabricates a step, a package that returns plausible nonsense — each is worse than the
absence of the feature, because each is invisible.

---

# Architecture

Deliberately under-specified. The boundaries are the commitment; the contents of each box are for the
issues that implement them to decide.

```
┌─────────────────────────────────────────────────────────────────┐
│ APPLICATIONS IDEs · notebooks · teaching · engineering │
├─────────────────────────────────────────────────────────────────┤
│ NATURAL LANGUAGE text · LaTeX · speech · images → Entity │
├─────────────────────────────────────────────────────────────────┤
│ PLANNING goals · budgets · portfolios · diagnosis │
├─────────────────────────────────────────────────────────────────┤
│ STRATEGY ENGINE tactics · search · heuristics · costs │
├─────────────────────────────────────────────────────────────────┤
│ KNOWLEDGE GRAPH objects · theorems · prerequisites │
├─────────────────────────────────────────────────────────────────┤
│ ALGORITHMS polynomials · integration · limits · sets │
├─────────────────────────────────────────────────────────────────┤
│ REWRITE ENGINE rules as data · canonicalisation · cost │
├─────────────────────────────────────────────────────────────────┤
│ EXPRESSION TREE immutable Entity · domains · provenance │
└─────────────────────────────────────────────────────────────────┘

cross-cutting, present at every layer:
provenance · assumptions · settings/context · budgets · serialization
```

Two rules govern the picture, and they are the whole architectural content of it:

1. **Every layer is useful on its own.** Someone who wants only the expression tree and the rewrite
engine gets a fast, boring, dependency-light library — and that must stay a supported way to use
AngouriMath forever. Nobody should have to accept a planner to get a parser.
2. **No layer reaches around the layer below it.** The strategy engine does not construct nodes
directly; the NL layer does not call solvers directly. Every shortcut of this kind is a place the
system later cannot be extended, replaced or verified.

Layer by layer, with the *non*-responsibilities stated, since those are what erode:

**Expression tree.** The immutable `Entity` hierarchy, plus what a node knows about itself: domain,
assumptions, and where it came from. Not responsible for deciding anything is "simpler".

**Rewrite engine.** Rules as data — matchable, enumerable, attributable, prioritisable — with
canonicalisation, cost comparison, and termination as properties of the engine rather than habits of
each rule author. Not responsible for knowing which rules are about trigonometry.

**Algorithms.** The deep classical machinery: the polynomial layer (multivariate GCD, resultants,
factorisation), Risch, Gruntz, Gröbner, quantifier elimination, number theory. Each written *against*
the rewrite engine so its internal knowledge is expressed as reusable rules and tactics wherever it
can be. Not responsible for deciding when it should be invoked.

**Knowledge graph.** What is true, what it is true about, what it depends on, and where it was
published. Queryable: *what do I know about this object?* Not responsible for searching.

**Strategy engine.** Given a goal and a state, decide what to try next; combine tactics; spend a
budget; know when to give up and why. Not responsible for guaranteeing anything is provable.

**Planning.** Above strategy: decompose goals, run portfolios, allocate effort across approaches,
and — critically — produce a **structured diagnosis** on failure. Not responsible for talking to
humans.

**Natural language.** Ambiguous input to unambiguous `Entity`, always with the interpretation shown
back for confirmation (which is exactly what the round-trip contract buys us). Never a shortcut into
the lower layers. Not responsible for mathematics.

**Applications.** Everything anyone builds. The measure of the whole design is how little of the stack
an application has to understand.

## Packaging, and what must never regress

Three constraints cut across every tier below. They are not roadmap items to be scheduled; they are
conditions on all of them. A tier that violates one has failed regardless of what else it delivered.

**The common case pays for nothing it does not use.** The layer split above is a *code* boundary; it
needs a matching *distribution* boundary, so that common-use paths and edge-case machinery ship
separately and someone who wants to parse and simplify never downloads a planner, an SMT bridge or a
geometry pack. We already have the pattern — kernel, `FSharp`, `Interactive`, `Terminal`, `CPP` and
`Experimental` are separate packages — and the roadmap should extend it rather than grow one
ever-larger assembly. The honest cost: every boundary widens the version matrix, the CI time and the
number of ways a user can assemble something we never tested, so a split earns its place only where
the boundary is load-bearing. Decide these deliberately and early; published package boundaries are
close to immovable. (Raised by @darkfader in this thread.)

**Speed and memory on popular use cases are measured, not hoped for.** Parsing, `Simplify`, `Solve`
and differentiation on textbook-sized input are the paths almost every caller is on, and every tier
below adds machinery that could tax them. The corpus runner and the inter-version benchmark
([#529](https://github.com/asc-community/AngouriMath/issues/529),
[#500](https://github.com/asc-community/AngouriMath/issues/500)) exist to make a regression there a
build failure rather than a bug report six months later. The fast path must survive as a path: a
rewrite graph, a planner or a knowledge-graph lookup that cannot be bypassed for the easy case is a
design error, not a performance to-do. (Raised by @Happypig375 in this thread.)

**Correctness coverage grows with the surface.** Each tier adds ways to be wrong that the tier below
could not express — a bad strategy choice, a mis-stated theorem, a pack asserting a false identity.
Tests, property checks and the *wrong / error / timeout* counts have to grow with the architecture, not
after it, because a reasoning platform that is merely usually right is worth less than a library that
is narrowly right.

---

# Roadmap

Ten capability tiers, ordered by **dependency**, not by date. They will overlap heavily in practice;
a tier is "reached" when the infrastructure it names is something other work can rely on. Nothing here
implies a release schedule, and nothing here is a promise.

## Where the tiers stand

Measured against `6b93b401` (master, package version 2.3.0) on 2026-08-23. **A published package
version does not mean the tier of the same name is reached** — 2.0.0 through 2.3.0 are shipping
versions, and the note on each says which tier it did and did not advance.

| tier | state |
|---|---|
| **1 — a symbolic engine worth building on** | **Required infrastructure built, with one row overstated.** Polynomial layer ([#918](https://github.com/asc-community/AngouriMath/pull/918), [#923](https://github.com/asc-community/AngouriMath/pull/923), [#927](https://github.com/asc-community/AngouriMath/pull/927)) — **square-free decomposition is multivariate as of [#1054](https://github.com/asc-community/AngouriMath/pull/1054)** — `p / gcd(p, dp/dx)` holds in any coefficient ring and the multivariate representation already had the derivative, the recursive GCD and exact division, so only the code was univariate. **Factorisation is multivariate, and what is left is a degree budget rather than a variable count.** [#1053](https://github.com/asc-community/AngouriMath/pull/1053) takes the content out first, so `Factor("x * y + y", "x")` is `y * (x + 1)` where it was a refusal; [#1055](https://github.com/asc-community/AngouriMath/pull/1055) factors the genuine two-variable case by **Kronecker's substitution**; and [#1058](https://github.com/asc-community/AngouriMath/pull/1058) generalises it, because nothing in the method was about two. Packing an exponent pair as `i + s·j` is a two-digit numeral in radix `s`, and an exponent vector of any length is a numeral in **mixed radix** — radices `d_i + 1`, place values `s_0 = 1`, `s_(i+1) = s_i · (d_i + 1)`. A factor's degree is bounded by the polynomial's in every variable *because it divides it*, so injectivity survives the generalisation untouched. Measured: `Factor("x ^ 2 - (y + z) ^ 2", "x")` is `(x + y + z) * (x - y - z)` and `Factor("(x + y) * (x + z) * (x + w)", "x")` is `(x + y) * (w + x) * (x + z)`. Every candidate is checked by exact division, so a refusal is a possible answer and a wrong one is not — and since [#1059](https://github.com/asc-community/AngouriMath/pull/1059) **"it does not factor" is an answer too**, said by handing the polynomial back, because the substitution *proves* irreducibility rather than merely failing to find a factorisation. Reporting that proof as `null` had been throwing the content out with it: `Factor("x * y + y * z", "x")` was a refusal although `y * (x + z)` was already half-found. The proof's precondition is checked rather than assumed — a trial division that ran out of room is not a "does not divide", and only the latter is evidence. **Remaining on this line:** the image has degree `Π (d_i + 1) - 1`, a *product* and not a sum, against the univariate factoriser's 32 — three variables of degree 2 fit and four do not, and `x ^ 12 - y ^ 12` is past it in two. Lifting that is **Hensel lifting with an evaluation homomorphism**, still the one piece of tier 1 that is a project rather than a change — and [#1064](https://github.com/asc-community/AngouriMath/pull/1064) settles *why* by measurement rather than by inheritance. `IntegerPolynomial.MaxDegree` is 32 where the machinery underneath affords 64, which looks like a free doubling of an exponent budget that is a *product* and so worth a whole variable of reach; doubled, **nothing new factors**, at images of degree 34 to 56 sitting inside the raised ceiling. The limit is the method: the substitution's images **over-factor** — `x ^ 7 - y ^ 7` becomes `t ^ 7 (1 - t ^ 49)`, whose factors are cyclotomic — so the recombination is exponential in a count the substitution itself inflates, which is the cost that bound was set to guard. Not inflating it is the different algorithm. *The resultant's want of a production caller was still recorded here and had stopped being true* — [#1017](https://github.com/asc-community/AngouriMath/pull/1017) gave it one, `PolynomialSignTable` taking the discriminant to place its sample points, and item 43 already said so. Canonical form specified and implemented ([#928](https://github.com/asc-community/AngouriMath/pull/928), [#933](https://github.com/asc-community/AngouriMath/pull/933), [#935](https://github.com/asc-community/AngouriMath/pull/935)). Corpus gate reporting solved / wrong / error / timeout per commit ([#945](https://github.com/asc-community/AngouriMath/pull/945)). Public surface documented ([#943](https://github.com/asc-community/AngouriMath/pull/943), [#944](https://github.com/asc-community/AngouriMath/pull/944)). **Pattern matching as data ([#248](https://github.com/asc-community/AngouriMath/issues/248)): something runs on it now.** This row read *"nothing runs on it"* and named the reason — the one exchange ever made cost about 5% of `Simplify` and was reverted, and 5% for one of thirty sets does not scale to thirty. That number was a property of the matcher rather than of the idea: `NodePattern.IsDeterministic` was recomputed on **every attempt**, walking the whole pattern tree behind a delegate before any matching began, so the case that does the least work — a rule that does not fire — paid the most for it. Settled once instead ([#1050](https://github.com/asc-community/AngouriMath/pull/1050)), a miss goes 29.99 ns → 13.48 ns and a whole pass 1182.9 ns → 659.9 ns, at identical allocation. Re-measured against `Simplify` itself with a control arm that is the `switch` again, the exchange is **−0.6% where the control differs from its own source by −1.1%**, and allocation is +0.04% — so [#1052](https://github.com/asc-community/AngouriMath/pull/1052) runs `DivisionPreparing` and `CollapseMultipleFractions` as data and [#1060](https://github.com/asc-community/AngouriMath/pull/1060) adds `InvertNegativePowers` and `InvertNegativeMultipliers`. **14 of 30 sets, not 0**, and a commutative pattern is proven to agree with the arms it replaces ([#1066](https://github.com/asc-community/AngouriMath/pull/1066)) — eight arms become three, twice — which is what the three largest collapses left on the list all turn on. Each is one whose data form is *proven* to agree with the `switch` it mirrors over generated expressions, which is the precondition for exchanging one for the other. **And the corpus that proof runs on is part of it.** With `-1` as its only negative leaf the negative-power rule fired on **7 of 1,399** expressions, which is agreement between two things that barely ran; the threshold in the agreement test exists for exactly that and caught it. Enriched, the two sets fire 27 and 56 times of 3,417, and the sets already checked still agree — so nothing had been hiding behind the thin leaves. **Remaining:** the other 16, and they are a work-list rather than a count — `work/rulecheck` now lists every set with its arm count, how many arms need something the matcher cannot express, and how many share a replacement with an earlier arm. **Every one of them is writable today**, and the first version of this row said otherwise. It named eight sets as needing type alternation or a negated pattern in the matcher; a **predicate on a hole** says all three constructs — `Sumf or Minusf` is `Any(n, e => e is Sumf or Minusf)`, `var x and not Integer(1)` is a predicate, `Rational and not Integer` is a predicate on a typed hole — and `Any(name, where)` has been there since the matcher was written. `PerfectSquare` was converted to prove it rather than to argue it. So what stands between every remaining set and the exchange is the agreement proof, which is a test rather than a design. `Boolean` is the largest collapse on the list: 36 arms of which 20 share a replacement. `RationalizeDenominator` has **0** arms, the registry having declined its shape, which is a generator gap rather than a matcher one; and the `switch` cannot go even for these two, because `RuleRegistryGenerator` reads `PatternSource` and `SourceLine` off a `switch`'s arms and cannot yet read a rule written as data ([#825](https://github.com/asc-community/AngouriMath/issues/825)). **Expression metadata was retired** as having no consumer; that was measured on the limit case only, and [#721](https://github.com/asc-community/AngouriMath/issues/721) is still open. |
| **2 — the rewrite graph** | **A rule can now be read backwards; the graph is still not built.** The registry is done (item 50), the e-graph is honestly evaluated with a negative recommendation (item 51), and the first item this row used to list is delivered: [#1043](https://github.com/asc-community/AngouriMath/pull/1043) makes `MatchPattern` a *template* as well as a pattern, so a rule whose two sides are both patterns has two directions and swapping them is the reversal. **13 of the 14 rules expressed as data reverse; the Pythagorean identity does not**, because `1` does not say which angle it came from — and the type says so rather than a comment, `Reversal` being derived and never declared. `Simplify` is unchanged: allocation identical to the byte, and −0.13% on time against a byte-identical control arm that differed from its own source by 0.47%. **Remaining, in dependency order:** *this mechanism has no production caller* — the consumer is the e-graph's inverse-pair table, and until something consumes it this is a capability rather than a use; only 14 rules are data against 405 addressable `switch` arms, and *the reason recorded here for that had stopped being true* — the +5% that reverted the last exchange was `NodePattern.IsDeterministic` being recomputed on every attempt, settled once in [#1050](https://github.com/asc-community/AngouriMath/pull/1050), after which the exchange measures −0.6% against a control differing from its own source by −1.1% and a run of PRs now runs **14 of 30 sets** as data ([#1052](https://github.com/asc-community/AngouriMath/pull/1052), [#1060](https://github.com/asc-community/AngouriMath/pull/1060), [#1061](https://github.com/asc-community/AngouriMath/pull/1061), [#1065](https://github.com/asc-community/AngouriMath/pull/1065), [#1066](https://github.com/asc-community/AngouriMath/pull/1066)) at a re-measured cost of **+0.14% allocation and nothing outside the noise floor on time** — six samples each, medians 0.12% apart where the same binary spreads 1.90%. What actually gates the other 28 is per-set proof that the data form agrees with the `switch` it mirrors, and [#825](https://github.com/asc-community/AngouriMath/issues/825): `RuleRegistryGenerator` reads `PatternSource` and `SourceLine` off a `switch`'s arms, so the `switch` cannot be deleted even where it no longer runs. **Per-rule soundness was recorded here as absent and is not** — `MatchedRule` carries a `Soundness` and it already distinguishes: 2 of the 14 data rules are `Sound` (the shared factor, and `sin² + cos² = 1`, which holds for every complex argument) and 12 are `SoundUnderAssumptions`. What is uniform is the *set* grain — all 31 `RewriteRuleSet` declarations say `SoundUnderAssumptions` — so every rule still written as a `switch` inherits its set's tier and has none of its own. That is the same line as the one above rather than a second one: a rule gets a tier by becoming data; folding on insertion, since 13–34% of the e-nodes in every runaway graph are a neutral element applied to something; and a cost model that reaches an API rather than an ambient setting. **Termination is no longer among them** — [#1057](https://github.com/asc-community/AngouriMath/pull/1057) moves the check out of the workspace and into the suite, asking it twice because the two questions have different answers: iterated **alone** every set settles except `Power` and `NumericNeat`, and with the normalisation between passes — how `Simplify` runs them — every set settles except `Common`. Both lists are asserted **in both directions**, so a set that starts cycling fails and a set that stops cycling fails too, which is what a workspace report cannot do. It found a genuine three-cycle in `Common` on `-x * 1/2` — `Mulf(-1/2, x)`, `Mulf(-1, Divf(x, 2))`, `Divf(Mulf(-1, x), 2)`, three trees printing as two strings — recorded as [#1056](https://github.com/asc-community/AngouriMath/issues/1056) rather than fixed, since `Simplify` bounds its own iteration and choosing an orientation for a set that runs on nearly every simplification is a decision. Item 78's package decision is no longer among them — it is made ([#1023](https://github.com/asc-community/AngouriMath/pull/1023)), and it puts the e-graph in the kernel behind an explicit entry point, because its cost is runtime memory and no boundary fixes that. |
| **3 — the theorem graph** | **Not started.** No ontology, no statements-as-data beyond `Impliesf`/`Providedf`, no dependency graph, no citations, no query layer. The one algebraic-structure type in the tree is an `internal` semiring with two instances, used to parameterise coefficient arithmetic — not an ontology. |
| **4 — the strategy engine** | **Not started, but its budget object now exists.** `Transformation` with `Then`/`Repeat`/`UntilStable` is still `Entity → Entity?`, not `Goal → Subgoal[]`; there is no `OrElse`, so no alternatives and no backtracking. No search, no portfolio. What has changed is the budget: `WorkBudget` is a value with an inherited ledger and a `BudgetOutcome` naming *where* and *why* ([#1035](https://github.com/asc-community/AngouriMath/pull/1035)), so [#896](https://github.com/asc-community/AngouriMath/issues/896)'s gap — a resource limit that names itself and is then discarded at the boundary — is closed for Gröbner and open everywhere else. Structured failure was real inside the transformation layer and absent outside it, and **that chokepoint is closed**: `Solve` returned an empty set both for "no solutions" and for "I gave up", and since [#1046](https://github.com/asc-community/AngouriMath/pull/1046) the two exits that mean nothing settled this answer with the equation as a set builder, while an emptiness that was established still answers `{ }` ([#1036](https://github.com/asc-community/AngouriMath/issues/1036) step 1). The remaining steps of #1036 are the other givers-up. A survey for it found roughly 70 sites that give up on a resource, of which exactly one threw and exactly one recorded which limit fired — with four where exhaustion is currently rendered as a mathematical claim. |
| **5 — proofs, derivations and explanations** | **The first piece exists; the object it needs does not yet.** `DerivationPath` ([#1012](https://github.com/asc-community/AngouriMath/pull/1012)) is an ordered path from the input to the answer — steps with `Before`, `After`, the rule set that fired and the count of expressions explored, the shortest route where several reached the answer, ties settled by record order rather than by hash. That closes the blocker this row used to name: the recording is no longer the rewrites of every candidate including the losers. What tier 5 asks for beyond it is absent, and the two gaps are specific. **Justification is per rule *set*, not per step** — `Relation` and `Soundness` are read off the set, all 30 of which declare the same tier, so a step cannot say why *it* is allowed. **Assumptions are not carried at all**: a step does not record what it assumed, so the path cannot be checked, only replayed. Nothing reverses (item 49), and no step renders as a sentence. |
| **6–10** | Not started. Each is behind the tier below it. |

### The three standing conditions

| | |
|---|---|
| The common case pays for nothing it does not use | **Still drifting on paper, but the mechanism that answers it turns out to be cheaper than a package split.** Four published packages, unchanged. The kernel is 211 files and 53,665 lines and has absorbed Gröbner, monoid algebra, quantum, the polynomial layer and the transformation layer across three releases — one correction, since the audit: **SymPy export is not among them**, it has been an abstract member of `Entity` since before `v1.4.0`. Two corrections to item 78's own premise stand: `Experimental` is a folder inside the kernel rather than a package, and the C++ wrapper is not published. What has changed is the answer available: [#1016](https://github.com/asc-community/AngouriMath/pull/1016) marks the assembly `IsAotCompatible` (which implies `IsTrimmable`), so a caller who trims gets only the code they reach — and measurement for the item 78 document ([#1008](https://github.com/asc-community/AngouriMath/issues/1008), [#1023](https://github.com/asc-community/AngouriMath/pull/1023), both open) found that a trimmed app which only parses and one that parses *and* calls `Simplify` produce a **byte-identical** kernel assembly, with the whole spread from narrowest to broadest use at 8.4%. Splitting managed code out of the kernel would therefore buy a fraction of that, against a permanent version matrix. The condition is real; a package boundary is not the instrument for it, and trimming is. |
| Speed and memory measured, not hoped for | **Met, and now as a mechanism.** Every release since 2.1.0 publishes a measured pair on one machine, and the pair for 2.2.0 caught something real. Item 80's threshold now exists ([#1014](https://github.com/asc-community/AngouriMath/pull/1014)): `PerformanceGate` reads a committed baseline and **fails the build on allocation moving more than 3%**, with time gated only above 3× because a shared runner's wall clock is a property of whoever else is on the host. The honest caveat is that this gates allocation, not speed — a change that is 40% slower and allocates the same passes, and is reported for a human rather than failed. |
| Correctness coverage grows with the surface | **Met.** 7,533 tests passing, a four-way corpus gate on every commit, and rule-grain confluence in the suite. The caveat worth stating: the in-CI corpus is 40 problems, and none of the twelve harnesses in the analysis workspace runs in CI. |

## v1.0 — A symbolic engine worth building on

**Goals.** Be the best symbolic engine in .NET, and — more important for everything that follows —
be one with foundations that later layers can stand on without prying. Most of the currently open
simplification and solving issues are not independent bugs; they are the same missing infrastructure
seen from different angles.

**Required infrastructure.**
- A real polynomial layer: multivariate GCD, resultants, factorisation over ℚ and finite fields,
square-free decomposition. This one item unblocks a large fraction of the open tracker.
- Canonical forms with a *written specification* of what canonical means for each node class, and
a stated distinction between canonical and "simplest".
- Pattern matching as a data structure, not a `switch`: matchable, enumerable, testable, with
commutative and n-ary matching handled by the engine ([#248](https://github.com/asc-community/AngouriMath/issues/248)).
- Expression metadata: assumptions and domains that travel with a node instead of being re-derived.
- A performance and correctness harness that reports **solved / wrong / error / timeout** on a fixed
corpus, per commit ([#529](https://github.com/asc-community/AngouriMath/issues/529),
[#500](https://github.com/asc-community/AngouriMath/issues/500)).

**Major deliverables.** The polynomial layer; a specified canonicaliser; the pattern-matching engine;
API and behaviour consistency sweeps; documentation of every public surface
([#585](https://github.com/asc-community/AngouriMath/issues/585)); the measured corpus.

**Example issues.** [#185](https://github.com/asc-community/AngouriMath/issues/185) (polynomial
simplifier with replacements), [#205](https://github.com/asc-community/AngouriMath/issues/205) (surds),
[#204](https://github.com/asc-community/AngouriMath/issues/204) (roots vs fractional powers),
[#203](https://github.com/asc-community/AngouriMath/issues/203) (collapse must collapse),
[#176](https://github.com/asc-community/AngouriMath/issues/176),
[#740](https://github.com/asc-community/AngouriMath/issues/740),
[#224](https://github.com/asc-community/AngouriMath/issues/224) (caching linear children),
[#392](https://github.com/asc-community/AngouriMath/issues/392) (`FastString`),
[#381](https://github.com/asc-community/AngouriMath/issues/381) (characteristic polynomial),
[#526](https://github.com/asc-community/AngouriMath/issues/526) (compile matrices).

**Expected challenges.** Canonical vs simplest is genuinely unresolved in the literature and we will
have to take a position and document it. Every canonicalisation change moves printed output, which
means [BREAKING-CHANGES.md](https://github.com/asc-community/AngouriMath/blob/master/BREAKING-CHANGES.md)
entries and a lot of test churn — measured on real builds, per AGENTS.md, not read off diffs. And the
polynomial layer is weeks of work that closes nothing visible until it lands, which is exactly the
kind of work a volunteer tracker under-supplies.

## v2.0 — The rewrite graph

**Goals.** Turn simplification from a procedure into a *searchable space*. Today "simplify" means
"apply a curated list of rewrites in a curated order and hope". That cannot be reasoned about,
extended safely, or explained.

**Required infrastructure.**
- Rules as first-class data: identity, name, direction, applicability conditions, justification tier,
provenance, cost effect.
- A rewrite graph — the set of expressions reachable from a start point, with edges labelled by rule.
Equality saturation / e-graphs are the obvious candidate mechanism and should be evaluated honestly
against memory cost on real expressions.
- A cost model that is comparable across domains and is *data*, so callers can supply their own
(smallest tree, fewest radicals, numerically stablest, most readable to a student).
- Rule priorities and conflict resolution, with confluence and termination checked by tooling rather
than asserted by authors.
- Transformation metadata rich enough that v5.0 can render a step as a sentence.

**Major deliverables.** The rule registry; the rewrite graph with pluggable extraction; a
canonicalisation framework built on it; a rule-authoring guide; the confluence/termination checker.

**Example issues.** [#28](https://github.com/asc-community/AngouriMath/issues/28) (collect intermediate
pattern replacements), [#195](https://github.com/asc-community/AngouriMath/issues/195) (aggressive
replacement), [#322](https://github.com/asc-community/AngouriMath/issues/322),
[#327](https://github.com/asc-community/AngouriMath/issues/327) (Piecewise patterns),
[#415](https://github.com/asc-community/AngouriMath/issues/415) (simplify intervals),
[#270](https://github.com/asc-community/AngouriMath/issues/270).

**Expected challenges.** Combinatorial explosion is the whole difficulty — a rewrite graph without
aggressive bounding will eat all memory on textbook input. Rule interactions become emergent and hard
to attribute. And there is a real risk of a slower `Simplify` for the common case, which is
unacceptable; the fast path must survive as a path.

## v3.0 — The theorem graph

**Goals.** Give the system a memory. Facts, the objects they are about, and the dependencies between
them — stored, queryable, cited, and versioned, rather than compiled into method bodies.

**Required infrastructure.**
- A mathematical ontology: objects, properties, relations, structures, with room for
[#440](https://github.com/asc-community/AngouriMath/issues/440) (groups, rings, fields) and
[#510](https://github.com/asc-community/AngouriMath/issues/510) (generic math structure) to be its
first real inhabitants.
- Statements as data: hypotheses, conclusion, quantifiers
([#225](https://github.com/asc-community/AngouriMath/issues/225)), applicability conditions.
- A dependency graph — what a theorem needs, what it implies, what it specialises.
- Provenance: a citation for every fact, and a trust level.
- A query layer: *what do I know about this object / this shape of expression / this structure?*

**Major deliverables.** The graph store and query API; a seed corpus of classical theorems with
citations; conditions expressed as `Entity` statements so they are checkable by the engine we already
have; the first algorithm that consults the graph instead of hard-coding what it knows.

**Example issues.** Formalise the trigonometric identity set as graph entries; encode convergence
criteria; encode branch-cut conventions as first-class facts (DLMF-cited) instead of comments; express
domain-membership lemmas behind [#721](https://github.com/asc-community/AngouriMath/issues/721) and
[#719](https://github.com/asc-community/AngouriMath/issues/719).

**Expected challenges.** Ontology design is where projects like this die — too abstract and nothing
can be expressed, too concrete and it must be redone. Mitigation: never build ontology without a
consumer in the same PR. Also, the graph must not become a second, divergent statement of what the
code already believes; where both exist, the graph is the source and the code reads it.

## v4.0 — The strategy engine

**Goals.** Decide what to try next, deliberately and under a budget, instead of running a fixed
cascade of attempts.

**Required infrastructure.**
- Tactics: named, composable transformations of a goal into subgoals, with success and failure
semantics — plus combinators (`then`, `orElse`, `repeat`, `first`, `bounded`).
- Search over the rewrite graph and the tactic space: best-first, iterative deepening, and heuristic
guidance, with the guidance pluggable (this is where a learned model plugs in at v8.0).
- Budgets as first-class values: time, nodes, memory, rule applications — inherited by subgoals,
observable in results, and honoured cooperatively
([#373](https://github.com/asc-community/AngouriMath/issues/373)).
- **Structured failure.** A failure is a value describing where the search stopped and what would have
unblocked it — not `null` and not an unevaluated node with no story.
- Portfolio execution: run several approaches, take the first good answer, record what the others did.

**Major deliverables.** The tactic library covering what our solvers do today; the search engine;
the budget system; failure diagnosis; the first measurable result — the corpus solved count going up
with *no* new mathematics, purely from better strategy.

**Example issues.** Re-express the existing equation solvers as tactics; a solver portfolio for
[#278](https://github.com/asc-community/AngouriMath/issues/278) corner cases;
[#357](https://github.com/asc-community/AngouriMath/issues/357) (dependency reduction) as a planning
step; [#744](https://github.com/asc-community/AngouriMath/issues/744) (a power of a polynomial solved
by inverting into itself) as a case where search must detect that it has returned to a previous state.

**Expected challenges.** Search quality is where honesty is hardest to hold: a heuristic that
"usually" works will produce confident wrong answers unless every tactic's soundness tier is respected
by the search. Loop and cycle detection over an infinite space. Reproducibility under a time budget —
which is why the budget must be in *work units*, not wall-clock, wherever an answer depends on it.

## v5.0 — Proofs, derivations and explanations

**Goals.** Make the derivation a first-class artefact — machine-checkable, human-renderable, and
audience-adjustable.

**Required infrastructure.**
- A derivation object: an ordered DAG of steps, each with the rule, the justification tier, the
assumptions used, and the before/after expressions.
- The step recorder with reversible trees ([#273](https://github.com/asc-community/AngouriMath/issues/273)) —
now finally cheap, because v2.0 made every step attributable and v4.0 made backtracking explicit.
- Proof templates: reusable shapes (induction, contradiction, case analysis, substitution-and-back,
squeeze) as data, so a derivation can be recognised as an instance of a known argument.
- Explanation rendering at a chosen level: primary school, secondary, undergraduate, research —
same derivation, different prose and different elision.
- A hint API: the *next* step, not the answer. (This single API is most of what an education product
needs, and we would be the only open library that has it.)

**Major deliverables.** The derivation type and its serialization; the step recorder; the template
library; the multi-level renderer; `Explain` and `Hint` on the public surface; LaTeX and prose output.

**Example issues.** Render a derivation as LaTeX; per-step assumption tracking (*"dividing by x-1,
which requires x ≠ 1"*) — note that we can already *express* that condition as a value, which is why
this is achievable; a `Why(step)` API; replay a serialized derivation and verify each step
independently.

**Expected challenges.** Derivations of interesting problems are large; storing and rendering them
needs care. Explanation quality is subjective and cannot be unit-tested the way an integral can —
expect to need human review as part of CI for a sample. And a derivation that is *technically*
complete but unreadable is a failure of the deliverable, not a documentation gap.

## v6.0 — The numerical and applied ecosystem

**Goals.** Cover the rest of working mathematics, with every new domain paying rent to the same
infrastructure rather than becoming a private silo.

**Required infrastructure.**
- A numerics layer bridged to the symbolic one: arbitrary precision, interval arithmetic (for honest
bounds rather than hopeful floats), and compilation as the crossing point
([#363](https://github.com/asc-community/AngouriMath/issues/363) for AOT).
- Optimization with symbolic derivative and constraint support — where symbolic differentiation stops
being a party trick and becomes the reason to choose us.
- Probability and statistics as symbolic objects: distributions, expectation and variance as algebraic
operators, symbolic moments, conditional independence.
- Geometry: symbolic points, lines, conics, transformations, with proofs available (Wu's method,
Gröbner-based provers) — sitting directly on the polynomial layer from v1.0.
- Graph theory and combinatorics, including symbolic generating functions.

**Major deliverables.** Each domain as a package, expressed in the shared tree, contributing rules to
the shared rewrite engine and facts to the shared theorem graph. A cross-domain benchmark suite.

**Example issues.** Analytical ODE solvers ([#241](https://github.com/asc-community/AngouriMath/issues/241));
more integral solvers ([#233](https://github.com/asc-community/AngouriMath/issues/233)); more limit
solvers ([#231](https://github.com/asc-community/AngouriMath/issues/231)); set, vector and matrix
equations ([#95](https://github.com/asc-community/AngouriMath/issues/95));
[#105](https://github.com/asc-community/AngouriMath/issues/105) (cross and dot on arbitrary entities);
symbolic linear algebra decompositions; a Pythagorean-triple solver
([#475](https://github.com/asc-community/AngouriMath/issues/475)) as a number-theory package
exercise.

**Expected challenges.** This is the tier where scope discipline breaks. The rule that saves it: a
domain package is only accepted if it *uses* the shared infrastructure and *contributes* to it. A
statistics package that ships its own private expression type has failed the review regardless of how
good its distributions are. Numerical work also brings a different testing culture — tolerances,
condition numbers, reproducibility across architectures.

## v7.0 — Formal verification bridges

**Goals.** Make our results checkable by systems that do not trust us.

**Required infrastructure.**
- Export of statements and derivations to Lean and Coq, and of side conditions to SMT solvers.
- A certified transformation subset: rules whose justification is complete enough to generate a
machine-checkable proof term.
- Proof certificates: an artefact a third party can validate without running AngouriMath at all.
- Import in the other direction: theorems proved elsewhere entering our knowledge graph with their
provenance and trust level intact.

**Major deliverables.** A Lean bridge (as an optional package, since the dependency is heavy); SMT
integration for the assumption discharge that already blocks
[#721](https://github.com/asc-community/AngouriMath/issues/721)-style work; a certified-rule subset
with its coverage measured and published; a certificate format.

**Example issues.** Emit Lean for a linear-equation derivation; discharge `Provided` conditions via
Z3; mark and count which rules in the registry are certifiable; validate an exported certificate in
CI on every release.

**Expected challenges.** The semantic gap is real: our `Entity` semantics are not Lean's, especially
around branch cuts, partial functions, and division. Proof assistants move fast and bridges rot.
Certifying everything is out of reach — so the honest deliverable is a *measured, published fraction*,
and a discipline of never claiming more.

## v8.0 — AI interfaces

**Goals.** Make the platform the reasoning substrate that agents and LLMs use instead of guessing —
and make it the thing that catches them when they do.

**Required infrastructure.**
- A reasoning API that accepts goals, constraints, budgets and context, and returns derivations or
structured failures. Stable, versioned, documented for machine consumption.
- Semantic search over the theorem graph: retrieve by mathematical content, not by string.
- Natural-language parsing to `Entity`, with the interpretation always echoed back for confirmation
(the round-trip contract is what makes this safe).
- An agent tool interface (MCP or equivalent) exposing the layers as callable, composable tools.
- A learned strategy component plugged into the v4.0 heuristic slot — never into correctness.
- Benchmarks: our corpus, competition sets, and textbook problems, reported as
solved / wrong / error / timeout, per model and per configuration.

**Major deliverables.** The reasoning API; the tool interface; the NL layer with confirmation; the
learned heuristic as an *optional* component with the deterministic path preserved; published
benchmark results.

**Example issues.** Extend [#717](https://github.com/asc-community/AngouriMath/issues/717) (SymPy
parity) and [#718](https://github.com/asc-community/AngouriMath/issues/718) (competition and textbook
problems) into corpora the reasoning API is measured on; natural-language query round-trip tests;
LaTeX-in / LaTeX-out; a verifier mode that takes someone else's claimed derivation and checks it step
by step.

**Expected challenges.** The central discipline: **a model may propose; only the platform may
conclude.** Any path where model output reaches a returned answer without passing a check is a
correctness hole with a friendly face. Natural language is irreducibly ambiguous, so confirmation is
mandatory, not a nicety. Learned components threaten determinism and must be quarantined behind the
heuristic slot, with a deterministic fallback that is always available and always tested.

## v9.0 — Knowledge packages

**Goals.** Let mathematics be distributed the way code is: versioned, dependency-resolved, community
maintained, trust-labelled.

**Required infrastructure.**
- A package format carrying nodes, rules, theorems, tactics, notation and tests together.
- Versioning and dependency resolution over *mathematical* dependencies, not just assemblies.
- Trust levels: certified, peer-reviewed, community, experimental — surfaced in every answer that
used them.
- Loading with the platform's guarantees intact: determinism, immutability, and no silent override of
kernel behaviour — and **statically declared** contents rather than contents discovered by scanning,
so that a packaged application can still be trimmed and AOT-published.
- Package-level testing and CI, so a knowledge pack can regress like code can.

**Major deliverables.** The format and loader; a registry; several reference packs (competition
number theory, undergraduate analysis, Euclidean geometry, engineering identities); the trust model,
end to end into the derivation output.

**Example issues.** Extract the current trigonometric rules into a pack as a proof of the format;
build a "high-school curriculum" pack; a conflict detector for packs asserting incompatible
conventions; provenance display in derivations.

**Expected challenges.** Trust and conflict are the hard parts — two packs can be individually
consistent and jointly contradictory, and the resolution must be principled rather than
load-order-dependent. Sandboxing arbitrary rules while keeping determinism is delicate. Registry
governance is a social problem, and it needs answering before the first pack ships, not after.

## v10.0 — Math OS

**Goals.** The layers are stable, documented, independently useful, and used by clients we did not
build. That is the whole of what "Math OS" means as an end state.

**Required infrastructure.** Stable versioned contracts at each layer boundary; conformance test
suites others can run against alternative implementations; long-term support commitments; governance
for the kernel and the registry; performance guarantees for the paths people build products on.

**Major deliverables.** A platform that serves, on the same foundations:
- **humans** — a terminal, notebooks, and an explanation layer that adapts to the reader;
- **IDEs** — symbolic verification of numeric code, unit and dimension checking, invariant checking,
refactoring assisted by algebraic equivalence;
- **AI agents** — a reasoning and verification substrate that is not a guess;
- **education** — hints, derivations, stepwise checking, curriculum-aware explanation;
- **research** — a scriptable platform for exploration, with formal export when a result matters;
- **engineering** — symbolic-numeric pipelines with honest error bounds.

**Expected challenges.** Every mature platform's problems: compatibility versus progress, breadth
versus depth, governance, and the pull toward feature accumulation once the interesting architecture
is finished. The counterweight is the guiding rule below, and the fact that everything here is
measured.

---

# Guiding Rule

**Build infrastructure, not isolated algorithms. Every new algorithm should make the next algorithm
easier to write.**

The question to ask in every review, and it applies to a five-line pattern as much as to a subsystem:

> After this change, is the *next* piece of mathematics cheaper to add than it was before?

Three concrete corollaries, all of which currently have teeth on our tracker:

**Prefer the change that closes many issues to the change that closes one.** A special-case pattern
that fixes one reported expression and adds one more entry to an unordered rule table has a negative
long-run value: it closes an issue and makes the table harder to reason about. The polynomial layer
closes dozens. Both are "work"; they are not the same work.

**When you find yourself encoding knowledge, ask where that knowledge belongs.** If your solver needs
to know that a substitution linearises a class of equations, that fact belongs in the rule registry or
the theorem graph, where the integrator and the limit code can also use it — not in a private branch
of your method.

**Fix the shape, not the instance.** Already the standard here (*"ask what else is the same shape, and
fix that too, or write down why not"*). At platform scale it becomes structural: if the same class of
bug keeps recurring, the missing thing is infrastructure that makes it unrepresentable.

And the counterweight, so this does not become an excuse for permanent architecture with no
mathematics in it: **infrastructure must be validated by a consumer in the same change.** A rewrite
engine with no rules ported, an ontology with no algorithm consulting it, a derivation type nothing
emits — these are not foundations, they are speculative code, and they rot faster than the
special-case patterns they were meant to replace.

---

# How contributors can help

Everything below is actionable now. Nothing waits on the roadmap being agreed. Difficulty is honest —
"easy" means genuinely a good first issue, not "easy for a maintainer". Where an existing issue
covers it, it is linked; where not, open one and link it here.

Labels to use: ` up-for-grabs`, ` up-for-grabs`, ` up-for-grabs`,
`Design document` for anything that needs agreeing before coding, and `Agentic goal` for long-running
tracked goals like this one.

### Easy — a first contribution, hours not weeks

1. Re-measure an old open issue on a current `master` build and close it with the measurement if it answers. Eleven issues turned out to be already fixed the last time someone swept the tracker; add any survivor to `AlreadyFixedIssuesTest.cs`.
2. Add a round-trip test for a node not currently covered by `StringizeRoundTripTest`.
**Status:** **largely obsolete as written.** `EveryNodeSurvivesEveryPipelineTest` reflects over every concrete `Entity` subtype and fails the day a new node is added, so hand-adding cases to `StringizeRoundTripTest` duplicates a check that already cannot go stale. The uncovered ground is *nested* forms — which is item 5.
3. Add a regression test for an open bug that is still open — the test alone is a contribution.
**Remaining:** Two open bug-labelled issues remain, and only one still reproduces: [#964](https://github.com/asc-community/AngouriMath/issues/964) returns `{ x }` for `derivative(y, x) + y - x`, which substitutes back to `1` rather than `0`. It has no test pinning it.
4. Write XML documentation with a worked example for one `MathS` member ([#585](https://github.com/asc-community/AngouriMath/issues/585)).
**Remaining:** 27 of 165 public non-type `MathS` members still have no ``. The wider surface is done: `AngouriMath.Extensions` went from **zero** of 89 to **all 89** ([#1029](https://github.com/asc-community/AngouriMath/pull/1029)), every printed value produced by running it and 89 of them pinned by tests, so the page cannot go stale in silence. The examples live in the *generators* for the two files that are generated — hand-added prose in a generated file is deleted by the next regeneration.
5. ~~Fix a `ToString`/`Latexise` precedence or parenthesisation case and add the round-trip test.~~
**Done** — [#1009](https://github.com/asc-community/AngouriMath/pull/1009). Six operators broke the round trip, not the two this item named: `implies`, `\`, `\/`, `in`, `mod` and `provided`. Five left the **right** operand unbracketed at a level the grammar folds left; `provided` is the mirror, the one infix operator the grammar folds **right**, so there it is the left operand that mis-associates — and it was found by testing the *expression* rather than the value, since by value it is safe. Four of the six moved an answer: `false implies (true implies false)` printed as text that read back `True` instead of `False`, and three set cases likewise.
6. ~~Make commit numbers in `version_performance_control.md` link to their commits ([#167](https://github.com/asc-community/AngouriMath/issues/167)).~~
**Done** — [#684](https://github.com/asc-community/AngouriMath/pull/684): every column header in `version_performance_control.md` links to its commit.
7. Add decimal and mixed-fraction output options ([#159](https://github.com/asc-community/AngouriMath/issues/159)).
8. ~~Extend the `Syntax.md` documentation to cover a grammar feature it currently omits.~~
**Done** — [#1041](https://github.com/asc-community/AngouriMath/pull/1041). The gap was derived rather than counted from this list: every function-open literal in the grammar (102) diffed against the page found **20 absent**, and the `atom` alternatives, lexer rules and `Parser.cs`'s token insertion added the rest — **15 features**, `sum` and `product` among them. 105 test cases pin the examples, comparing entities rather than strings.
9. Port one textbook exercise set into the test corpus with expected answers.
10. ~~Add a property-based test for an existing identity (differentiate an integral back; substitute a root; subtract two sides and simplify to zero).~~
**Done** — `Sources/Tests/UnitTests/Corpus/CorpusGateTest.cs` ([#945](https://github.com/asc-community/AngouriMath/pull/945)) runs all three named properties on every commit: a root substituted back, an antiderivative differentiated back, a simplification evaluated against its input.
11. ~~Improve one exception message so it names the offending sub-expression.~~
**Done** — [#1027](https://github.com/asc-community/AngouriMath/pull/1027). Re-measuring first corrected this item's own arithmetic: 9 of the 206 `throw new` occurrences are inside XML doc samples rather than code, so there are **197 real sites**. `Docs/Usage/Exceptions.md` went from three lines naming one exception type to documenting **all 25** that exist under `AngouriMathBaseException`, organised around the split a caller acts on — your input, a capability we lack, or a library defect that is not a catch target — with the overlapping pairs named and the one type nothing throws called out. Across 17 files the messages now carry what was passed: the source string on a parse failure, both shapes on a matrix mismatch, the expression on an uncompilable node. Interpolation sits inside the `throw` expression, so a path that does not throw pays nothing. (The exact before/after counts of interpolated versus constant messages depend on how a multi-line `throw` is counted; the figure this item started from, 7 of 206, is not reproducible under a pattern that also matches them.)
12. Add an F# wrapper for a C# API that lacks one.
**Remaining:** 18 C# areas have no F# wrapper. Separately, `Sources/Wrappers/AngouriMath.FSharp/Operators.fs` exists on disk but is not in the fsproj's compile list, so it ships nowhere — it is either a file to include and test, or a file to delete.
13. Add a Jupyter/`Interactive` example notebook for a feature that has none.
14. Tighten one analyzer diagnostic message or add a code fix for an existing analyzer.
15. Find and document a place where behaviour differs from SymPy, and say which is mathematically right — even without fixing it. This is real work and it is under-supplied.
**Remaining:** The catalogue exists — `work/sympyparity.md`, 80 probes over 23 areas — but it classifies by *capability*, not by which answer is mathematically right, and the rows where both sides answer differently are not adjudicated. Adjudication is what this item asks for and it is written down in only two places.

### Medium — a weekend to a few weeks, some internal knowledge

16. ~~Implement one classical algorithm behind the existing tracker: a logarithmic equation solver ([#246](https://github.com/asc-community/AngouriMath/issues/246)), exponential and logarithmic equations ([#214](https://github.com/asc-community/AngouriMath/issues/214)).~~
**Done** — both answer. `ExponentialSolver.cs` plus the fresh-variable substitution in `AnalyticalEquationSolver`; pinned by `AcceptedProposalsAlreadyImplementedTest.cs` ([#806](https://github.com/asc-community/AngouriMath/pull/806)). [#246](https://github.com/asc-community/AngouriMath/issues/246) is closed; [#214](https://github.com/asc-community/AngouriMath/issues/214) is open and should be closed on the measurement.
17. Surd simplification ([#205](https://github.com/asc-community/AngouriMath/issues/205)) — and decide and document the roots-versus-fractional-powers convention ([#204](https://github.com/asc-community/AngouriMath/issues/204)) while you are there.
**Remaining:** Rationalisation and surd simplification are done ([#791](https://github.com/asc-community/AngouriMath/pull/791)). [#204](https://github.com/asc-community/AngouriMath/issues/204) — the roots-versus-fractional-powers convention — is *described* in `SimplificationContract.md` as a deliberate major-version question and still not decided. Denesting is untouched.
18. ~~Make `Entity` serializable ([#323](https://github.com/asc-community/AngouriMath/issues/323)) — a v6/v8 prerequisite hiding in an old issue.~~
**Done** — [#1031](https://github.com/asc-community/AngouriMath/pull/1031), and the design position is the point: **the printed form is the serialisation and there is no second one.** A `JsonConverter` writes `Stringize()` and reads `MathS.FromString`, so it inherits the round-trip contract instead of creating one that can drift. The gap was real — `JsonSerializer.Serialize` threw *"a possible object cycle"* for every entity, `(Entity)3` included, so an `Entity` could not be a member of any serialisable type. Measuring the round trip over 112 of 115 node shapes also found [#1022](https://github.com/asc-community/AngouriMath/issues/1022) — `Stringize` printed no node's `Codomain`, so `domain(x, ZZ)` printed as `x` — since fixed by [#1047](https://github.com/asc-community/AngouriMath/pull/1047), which the converter inherited without a line of its own changing.
19. Cache `LinearChildren` ([#224](https://github.com/asc-community/AngouriMath/issues/224)).
20. `FastString` instead of `string` for `ToString` ([#392](https://github.com/asc-community/AngouriMath/issues/392)).
21. N-ary operators with variables ([#248](https://github.com/asc-community/AngouriMath/issues/248)).
**Remaining:** Sum and product landed ([#966](https://github.com/asc-community/AngouriMath/pull/966)), the first operators that bind a variable over a range. **Indexed union and intersection did not**, and [#248](https://github.com/asc-community/AngouriMath/issues/248) was closed with that half of its scope unbuilt.
22. Simplification patterns for `Piecewise` ([#327](https://github.com/asc-community/AngouriMath/issues/327)) and syntax for it ([#326](https://github.com/asc-community/AngouriMath/issues/326)).
**Remaining:** [#327](https://github.com/asc-community/AngouriMath/issues/327) is done ([#790](https://github.com/asc-community/AngouriMath/pull/790)). [#326](https://github.com/asc-community/AngouriMath/issues/326), the syntax, is untouched and no design decision is recorded.
23. ~~Interval simplification ([#415](https://github.com/asc-community/AngouriMath/issues/415)).~~
**Done** — [#677](https://github.com/asc-community/AngouriMath/pull/677) and [#793](https://github.com/asc-community/AngouriMath/pull/793). Meet, join and set-minus over intervals all reduce.
24. Subset operator ([#325](https://github.com/asc-community/AngouriMath/issues/325)) and extended `ConditionalSet` definitions ([#330](https://github.com/asc-community/AngouriMath/issues/330)).
25. Apply a transformation to every element of a set ([#322](https://github.com/asc-community/AngouriMath/issues/322)).
26. Characteristic polynomial ([#381](https://github.com/asc-community/AngouriMath/issues/381)).
27. Compile matrices ([#526](https://github.com/asc-community/AngouriMath/issues/526)).
**Remaining:** What landed is that an expression *mentioning* matrices whose value is scalar compiles. A matrix-*valued* expression still cannot be compiled, and a test asserts that it says so — which is exactly what this item asks for.
28. Inverse and derivative for factorial and gamma ([#171](https://github.com/asc-community/AngouriMath/issues/171)).
29. Differentiation with respect to functions ([#230](https://github.com/asc-community/AngouriMath/issues/230)).
30. Complex infinity, properly ([#217](https://github.com/asc-community/AngouriMath/issues/217)).
31. Parametric solutions ([#212](https://github.com/asc-community/AngouriMath/issues/212)).
32. Trigonometric equations expressed via arc functions ([#270](https://github.com/asc-community/AngouriMath/issues/270)).
**Remaining:** A single trigonometric function inverts correctly ([#792](https://github.com/asc-community/AngouriMath/pull/792)). A linear mixture — `3sin(x) + 4cos(x) = 2` — still falls through to the exponential solver and comes back in terms of `ln` and `i`.
33. Single-threaded timeouts ([#373](https://github.com/asc-community/AngouriMath/issues/373)) — and the budget object v4.0 needs is the same object.
**Remaining:** The object exists — `WorkBudget`, `BudgetLedger`, `BudgetOutcome` and an ambient `BudgetRecording` scope ([#1035](https://github.com/asc-community/AngouriMath/pull/1035)), with **one** consumer wired: Gröbner, whose fifteen exits are now individually named where they were one bare `false`. Wall clock is kept as a second axis and `IsDeterministic` is false exactly when a clock decided, which is Principle 3's requirement — the clock was never the problem, its invisibility was. **What remains is the other ~69 sites.** The survey behind that number is [#1036](https://github.com/asc-community/AngouriMath/issues/1036): of roughly 70 places the library gives up on a resource, exactly one threw and exactly one recorded which limit fired, and nothing read it.
34. A performance reporter ([#500](https://github.com/asc-community/AngouriMath/issues/500)) and inter-version benchmarking on key commits ([#529](https://github.com/asc-community/AngouriMath/issues/529)).
**Remaining:** The benchmark runs on every kernel-touching push and PR and now retains its results as an artefact. **No threshold fails a build**, no workflow has a schedule trigger, and the two destination repositories the performance-reporter issue names do not exist.
35. ~~Coverage for F#, Interactive and C++ ([#397](https://github.com/asc-community/AngouriMath/issues/397)).~~
**Done, with the caveat stated rather than hidden** — [#1038](https://github.com/asc-community/AngouriMath/pull/1038). Four legs report coverage, but not of the same thing: `csharp`, `fsharp` and `interactive` are managed coverage through `dotnet test`; `cpp` is gcov over the C++ wrapper, at 62.1% lines, because the C++ leg publishes NativeAOT and carries **no managed assembly** into CI for a collector to attach to. Managed coverage through the export path is not collected by any route tried, and the step fails on an empty report so the flag cannot go green on nothing. The same work found that `codecov-action@v5` silently ignores its `file:` input — `CSharpTest.yml` had been uploading whatever a workspace search found rather than the file it named.
36. ~~A corpus runner reporting solved / wrong / error / timeout as a CI artefact with per-commit history. Small, and the measurement half the roadmap depends on.~~
**Done** — [#1013](https://github.com/asc-community/AngouriMath/pull/1013). Both halves this item named now exist: `corpus-report.tsv` is uploaded per commit and per operating system with 90-day retention, and the per-commit history is `Sources/Tests/UnitTests/Corpus/corpus-baseline.tsv`, committed and diffed, so a verdict that moves fails the job rather than scrolling past in test output.
37. ~~Collect intermediate pattern replacements when simplifying ([#28](https://github.com/asc-community/AngouriMath/issues/28)) — the smallest real step toward explainability, open since the early days.~~
**Done** — `RewriteRecording` / `RewriteStep` ([#819](https://github.com/asc-community/AngouriMath/pull/819), [#978](https://github.com/asc-community/AngouriMath/pull/978)): a scope that collects each rewrite as `(rule set, rule, before, after)`, free when off, with `Derivation` cutting 270 raw rewrites to 6 on the issue's own expression. Attribution is per **rule**, not merely per set, since [#951](https://github.com/asc-community/AngouriMath/pull/951).
38. ~~Package `AngouriMath.Terminal` as a dotnet tool ([#627](https://github.com/asc-community/AngouriMath/issues/627)).~~
**Done, and it was done before the issue was filed** — `` with `amcli` since [#521](https://github.com/asc-community/AngouriMath/pull/521) (2021), packed and pushed by `Nuget.yml`. What is actually missing is documentation saying the package is `AngouriMath.Terminal` and the command is `amcli`.
39. A differential-equation corpus with known answers, ahead of a solver existing.
40. Compare us against another CAS on a fixed corpus and publish the table ([#184](https://github.com/asc-community/AngouriMath/issues/184)).
**Remaining:** The measurements exist — `work/libcompare`, `work/intbench` against Rubi, `work/sympyparity`. **None of them is published** anywhere a reader of this repository would find it.
41. Mine another open-source CAS's issue tracker for cases we get wrong ([#180](https://github.com/asc-community/AngouriMath/issues/180)).
**Status:** recorded in triage as not actionable as written. The useful version of it is an outside corpus (item 72) rather than tracker mining, and that is running.
42. Extend `ToSympy` to every node with a SymPy equivalent, with round-trip tests ([#717](https://github.com/asc-community/AngouriMath/issues/717)).
**Remaining:** Node coverage is effectively complete and the generated code now *runs* ([#1001](https://github.com/asc-community/AngouriMath/pull/1001)). The round-trip half is out of tree: the in-repo test checks paren balance and name binding only, because the suite cannot depend on a Python interpreter; `work/sympycheck` executes it and is not in CI.

### Hard — weeks to months, deep and high-value

43. **The polynomial layer**: multivariate GCD, resultants, factorisation over ℚ and 𝔽ₚ, square-free decomposition. The single highest-leverage piece of work on this list; a large part of the simplification tracker is waiting behind it.
**Remaining: the substitution's degree budget, and nothing else on this line.** Multivariate GCD, resultants and — since [#1054](https://github.com/asc-community/AngouriMath/pull/1054) — square-free decomposition all work; the resultant has a production caller. `MathS.Polynomials.Factor` refused every polynomial in more than one variable. [#1053](https://github.com/asc-community/AngouriMath/pull/1053) takes the content out first, so the ones that only needed their coefficients' common divisor removed are answered — `x * y + y` is `y * (x + 1)`. [#1055](https://github.com/asc-community/AngouriMath/pull/1055) answers the genuine case by **Kronecker's substitution**, and [#1058](https://github.com/asc-community/AngouriMath/pull/1058) writes that substitution in **mixed radix** so it is not about two variables: radices `d_i + 1`, place values `s_0 = 1`, `s_(i+1) = s_i · (d_i + 1)`, which writes each exponent as one digit of a numeral. A factor has degree at most `d_i` in each variable because it divides the polynomial, so the map is injective on every monomial that can appear in the polynomial or in any of its factors, whatever the length of the vector. Every candidate is checked by **exact division before it is kept**, which is why the substitution's over-factoring of the image cannot produce a wrong answer — only a refusal. Measured: `x ^ 2 - y ^ 2` is `(x + y) * (x - y)`, `x ^ 2 - (y + z) ^ 2` is `(x + y + z) * (x - y - z)`, `(x + y) * (x + z) * (x + w)` is `(x + y) * (w + x) * (x + z)`, `x ^ 2 * y + 2 * x * y + y` is `y * (x + 1) ^ 2`. **What is left is one ceiling and it is a refusal.** The image has degree `Π (d_i + 1) - 1`, a *product* and not a sum, so `IntegerPolynomial.MaxDegree` closes it quickly as variables are added: three of degree 2 fit (27) and four do not (81), and `x ^ 12 - y ^ 12` is past it in two variables alone. Raising it is **Hensel lifting with an evaluation homomorphism**, the one piece of tier 1 that is a **project rather than a change** — and [#1064](https://github.com/asc-community/AngouriMath/pull/1064) checked the cheap alternative rather than assuming it away. The degree bound could be doubled for free, since the machinery underneath affords 64 where the substitution is held to 32, and doubled it factors nothing new. The images **over-factor**: `x ^ 7 - y ^ 7` becomes `t ^ 7 (1 - t ^ 49)` with cyclotomic factors, so recombination is exponential in a count the substitution inflates. The bound was guarding exactly that, and moving it only moves where the refusal comes from. Factorisation over 𝔽ₚ exists (`PrimeFieldFactorization`) and is the univariate half of it. The other two gaps are closed by [#1017](https://github.com/asc-community/AngouriMath/pull/1017): the layer is `public` — `Factor`, `Gcd`, `Resultant`, `Discriminant`, `SquareFreePart` — so a limit is now an honest refusal rather than a silent absence, and **the resultant has a production caller**, `PolynomialSignTable` taking the discriminant to place the sample points of a polynomial sign table.
44. Risch integration, properly, with the elementary-integrability decision made and reported rather than guessed.
45. Gruntz's algorithm for limits, replacing pattern-driven limit work ([#353](https://github.com/asc-community/AngouriMath/issues/353), [#231](https://github.com/asc-community/AngouriMath/issues/231)).
**Remaining:** Gruntz is implemented and correct, but it **replaces nothing**: it runs only as the last fallback, only for an infinite destination, only two-sided, and only after divide-et-impera, indeterminate powers, l'Hôpital and rewriting have each declined. The 1,629 lines of pattern-driven limit descent are untouched and still first.
46. Gröbner bases and a real system-of-equations solver.
**Remaining:** Buchberger over degrevlex, FGLM to lex, and a system solver wired ahead of radical elimination — for **zero-dimensional ideals over ℚ only**, at most 8 variables and degree 127, and candidates are kept only if they reduce to exactly zero, so a system whose roots are decimals falls back wholesale. No public Gröbner surface, no ideal membership, no elimination ideals.
47. Quantifier elimination (CAD or a modern alternative) — the missing machinery behind most inequality work and behind [#225](https://github.com/asc-community/AngouriMath/issues/225).
48. Analytical ODE solvers ([#241](https://github.com/asc-community/AngouriMath/issues/241)).
49. The step recorder with reversible trees ([#273](https://github.com/asc-community/AngouriMath/issues/273)).
**Remaining:** **Nothing reverses.** The blocker named here is gone — [#1012](https://github.com/asc-community/AngouriMath/pull/1012) gives `DerivationPath` an ordered path from input to answer, each step carrying `Before`, `After`, the rule set and how many expressions were explored, so the losing candidates no longer contaminate the record. What is left is genuine reversibility, and it is worth saying where its consumer is: `Simplify` never backtracks, so nothing in simplification would read an inverse. The caller that would is the solver and tactic layer of tier 4, which is why this now sits behind item 64 rather than in front of it.
50. ~~The rule registry: turn the pattern set into enumerable, attributable data without regressing `Simplify` performance. A `Design document` first.~~
**Done** — 30 rule sets registered explicitly and enumerable through `RewriteRules.All`; **29 of them addressable at rule grain, 405 rules**, generated from the existing `switch` bodies by `Sources/Analyzers/RuleRegistryGenerator` rather than transcribed by hand ([#816](https://github.com/asc-community/AngouriMath/pull/816), [#818](https://github.com/asc-community/AngouriMath/pull/818), [#825](https://github.com/asc-community/AngouriMath/issues/825) for the design and the measurement that overturned the performance objection, then [#951](https://github.com/asc-community/AngouriMath/pull/951), [#968](https://github.com/asc-community/AngouriMath/pull/968), [#970](https://github.com/asc-community/AngouriMath/pull/970), [#973](https://github.com/asc-community/AngouriMath/pull/973), [#983](https://github.com/asc-community/AngouriMath/pull/983), [#987](https://github.com/asc-community/AngouriMath/pull/987)). No reflection, so the registry stays trimmable. **Remaining:** `RationalizeDenominator` is the one set the generator cannot read, because it is a method with branches rather than a `switch`.
51. ~~An e-graph / equality-saturation prototype over `Entity`, with honest memory measurements on realistic input and a recommendation either way.~~
**Done, with the recommendation it asked for, and the recommendation is *not yet*** — `work/egraph` in the analysis workspace. Firing each rule at every term of a class rather than one representative, only 7 of 16 textbook expressions saturate; 9 more than double and the worst by 7,143×. The obstacle is the rule set, not the e-graph: these rules were written for a directed, terminating pipeline, and saturation deletes the order that made them terminate.
52. ~~A pluggable cost model, with at least three implementations that visibly disagree.~~
**Done** — `CostModel` with four shipped models that visibly disagree ([#949](https://github.com/asc-community/AngouriMath/pull/949)), and extraction on the e-graph under all four found two cost-model defects `Simplify` structurally cannot reach; one is fixed ([#953](https://github.com/asc-community/AngouriMath/pull/953)). **Remaining:** no entry point *takes* a `CostModel` — selection is the ambient `MathS.Settings.ComplexityCriteria`, which drops the model's name and description at the boundary.
53. Groups, rings and fields as first-class ([#440](https://github.com/asc-community/AngouriMath/issues/440)), building on [#510](https://github.com/asc-community/AngouriMath/issues/510).
54. Functions and lambdas as entities ([#286](https://github.com/asc-community/AngouriMath/issues/286), [#495](https://github.com/asc-community/AngouriMath/issues/495)).
**Remaining:** `Lambda` and `Application` are real nodes, threaded through substitution, differentiation, printing, LaTeX and SymPy export, with capture-avoiding binding and working currying of built-ins. Missing is [#495](https://github.com/asc-community/AngouriMath/issues/495)'s syntax layer — no `=>` operator, no implicit application, single-parameter lambdas only — and a function-typed codomain.
55. Quantifiers ([#225](https://github.com/asc-community/AngouriMath/issues/225)).
56. Non-kernel functions and assembly-discovered types ([#321](https://github.com/asc-community/AngouriMath/issues/321), [#338](https://github.com/asc-community/AngouriMath/issues/338)) — the first real extensibility seam, and the ancestor of the v9.0 package format.
**Remaining:** [#321](https://github.com/asc-community/AngouriMath/issues/321) is done ([#961](https://github.com/asc-community/AngouriMath/pull/961)). [#338](https://github.com/asc-community/AngouriMath/issues/338) — looking a type up so it can be parsed from a string, which is *the* extensibility seam and the ancestor of the tier-9 package format — does not exist, and its collision with trimming and NativeAOT is still undecided.
57. ~~AOT-supported Linq compilation ([#363](https://github.com/asc-community/AngouriMath/issues/363)).~~
**Done** — [#1016](https://github.com/asc-community/AngouriMath/pull/1016). The four run-time lookups the compilation path used — `MathAllMethods` by name, `IsNaN` by name, and the operators and conversions found by reflecting over the operand type — are now tables of members named at compile time. Under the JIT nothing changes; under a trimmed or NativeAOT publish, six of the seven cases used to throw and the seventh took the process down, and all now answer.
58. Interval arithmetic with guaranteed bounds.
59. Arbitrary-precision special functions with documented branch cuts, checked against DLMF at the points where conventions disagree.
**Remaining:** The elementary functions are arbitrary-precision and their branch behaviour is measured by `work/boundcheck`. There is **one DLMF citation in the whole repository**, no written branch-cut specification, and no genuine special functions — no erf, zeta, Bessel, polylog, elliptic or Lambert W; `Gamma` is `Factorial(x - 1)` and real-argument only.
60. A symbolic-numeric bridge for optimization, using our derivatives.
61. A Lean export for a restricted but honestly-measured subset of derivations.
62. SMT-backed discharge of `Provided` conditions and domain assumptions ([#721](https://github.com/asc-community/AngouriMath/issues/721)).
63. Natural language to `Entity`, with the interpretation echoed back for confirmation.
64. A tactic language and search engine, with the existing solvers re-expressed as tactics and the corpus number moving with no new mathematics added.

### Research-grade — a paper's worth of work, and worth doing here

65. ~~What *is* canonical form for the class of expressions we support, and how does it relate to "simplest"? Take a position, write it down, and let the engine be checked against it.~~
**Done** — `Docs/Contributing/CanonicalForm.md` ([#928](https://github.com/asc-community/AngouriMath/pull/928)) takes the position: canonical is about identity, simplest is about presentation, and there is no canonical form for the whole language, because zero-equivalence is undecidable once `pi`, `exp`, the trigonometric functions and `abs` are in play (Richardson 1968). So it specifies a canonical form on a decidable sublanguage, a normalisation elsewhere that must not be mistaken for one, and a search not required to be canonical at all. Both halves implemented ([#933](https://github.com/asc-community/AngouriMath/pull/933), [#935](https://github.com/asc-community/AngouriMath/pull/935)) and checked by `work/canoncheck`.
66. Learned rewrite guidance that is provably confined to the heuristic slot and cannot affect soundness — with the deterministic path measured alongside it.
67. Proof-template extraction: recognise a derivation as an instance of a known argument shape.
68. Explanation quality: how do you evaluate a generated mathematical explanation, other than by asking people?
69. Conflict resolution between independently-consistent knowledge packages.
70. Semantic search over mathematical content — retrieval by meaning rather than by string.

### Non-code, and genuinely needed

71. Triage: reproduce open issues on current `master` and record the measurement. Every sweep of this finds issues that no longer exist.
72. Curate corpora: competition papers, textbook exercises, past papers, with answers and sources ([#718](https://github.com/asc-community/AngouriMath/issues/718)).
**Remaining:** The survey is done and it drew the licensing line. The CAS-suite half is running — 1,774 Rubi problems, 604 answered, none wrongly. The textbook, competition and past-paper half this item names is untouched.
73. Track SymPy, Maxima and SageMath releases for algorithms and behaviour worth matching ([#717](https://github.com/asc-community/AngouriMath/issues/717)).
**Remaining:** The SymPy half no longer goes stale on its own — `SymPyParity.yml` ([#1038](https://github.com/asc-community/AngouriMath/pull/1038)) installs the *newest* SymPy weekly, re-runs the 80 probes and **fails** if the version or any answer moves from a committed baseline, printing what changed. It passing on a GitHub runner is also cross-machine determinism evidence: 80 answers, different hardware and Python, matching exactly. **Maxima and SageMath are still not tracked at all**, and nothing here claims otherwise.
74. ~~Document conventions we have chosen and never wrote down — branch cuts, `mod` sign, ordering, the `arsinh` spelling and why.~~
**Done** — all four. Branch cuts as a *measured* table in `SimplificationContract.md`; the `mod` sign in `Syntax.md`; ordering in `CanonicalForm.md`; `arsinh` in `Syntax.md` and in a grammar refusal that carries the reason. **Remaining:** none. The associativity statement was corrected by [#1009](https://github.com/asc-community/AngouriMath/pull/1009) as part of making the printer state the grouping the grammar has. The variable-name rule was wrong in **four** ways rather than three — the fourth is Cyrillic, which the grammar accepts — and a third wrong statement nobody had noticed claimed `sinx` parses as `s * i * n * x`, where the lexer takes the longest match and returns one `Variable`. All corrected in [#1041](https://github.com/asc-community/AngouriMath/pull/1041), each with a probe that settles it.
75. Review a `Design document` issue. An architecture argued with by three people is worth more than one written by one.
76. Write tutorials, notebooks and worked examples for the website.
**Remaining:** The *verification* side is strong: `work/docsamples` compiles and runs all 84 wiki samples and checks each stated output. The authoring side is not moving — the two sample notebooks date from 2020 and one of them names no identifier that still exists.
77. Improve `AGENTS.md` and `CONTRIBUTING.md` as the practices here evolve — the discipline in those files is a load-bearing part of this vision, not paperwork around it.
**Remaining:** `AGENTS.md` is actively maintained. `CONTRIBUTING.md` is not: its documented build command fails as written, it points at a dead project board, and it says nothing about the harnesses, the corpus gate, `BREAKING-CHANGES.md` or reading a PR's thread before merging.

### Added from review of this issue

78. A `Design document` for the package split: which capabilities belong in the kernel package, which ship separately, and what the dependency rules between them are. Worth settling before v2.0 adds anything large, because published package boundaries cannot be moved afterwards.
79. A trimming and NativeAOT smoke test in CI: publish a small sample app with `PublishTrimmed` and NativeAOT, run it, and fail the build if the kernel path breaks or warns. This is a *medium* task that permanently protects [#363](https://github.com/asc-community/AngouriMath/issues/363), [#552](https://github.com/asc-community/AngouriMath/issues/552) and every extensibility decision above from being quietly undone.
**Done** — [#1016](https://github.com/asc-community/AngouriMath/pull/1016). `Sources/Tests/AotSmokeTest` publishes the managed kernel path both trimmed and NativeAOT and runs it, on three operating systems, with `ILLinkTreatWarningsAsErrors` and `IlcTreatWarningsAsErrors` set explicitly rather than inherited, so a warning fails the build. `AngouriMath` declares `IsAotCompatible` for `net8.0` and later. The gate on the C++ export surface that already existed stays; what was missing was the managed one.
80. Extend the benchmark suite to name the popular use cases explicitly — parse, `Simplify`, `Solve`, `Differentiate` on textbook-sized input, measured for both time and allocation — and wire a regression threshold into CI rather than leaving it to review ([#529](https://github.com/asc-community/AngouriMath/issues/529), [#500](https://github.com/asc-community/AngouriMath/issues/500)).
**Done** — [#1014](https://github.com/asc-community/AngouriMath/pull/1014). `PerformanceGate` reads the committed `performance-baseline.json` and fails the build. **Allocation is what it gates on**, at ±3%, because that is the metric a shared runner does not corrupt — three runs of one unchanged build spread at most 0.033% in allocation. Time fails only above 3×, which is a catastrophe gate rather than a performance one, and is called out for a human below that. It fails on an improvement too, exactly as the corpus gate does: the answer is to record the new number, not to widen the band.

---

## Closing

The strategy in one paragraph: **be the best symbolic engine in .NET first, and build every layer
above it so that the layer below stays independently useful.** Mathematica has more features and will
keep having more. What nobody has built is an *open* mathematical reasoning platform — inspectable,
composable, machine-readable, honest about what it does not know, and licensed so that anyone can
build on it. That is a different target, it is reachable from where we already stand, and the demand
for it is growing quickly now that agents want to do mathematics and cannot be trusted to do it
unaided.

Ten years is not an exaggeration of the timeline, and it is not a reason to wait. Every item in
*How contributors can help* is worth doing on its own merits today; the vision only decides which of
them to do first.

Comment with disagreements. Open issues for the pieces you want to own and link them here.

Start by reading the vision, AGENTS.md, coding_rules.md, and the linked checklist items, then inspect the repository paths and tests named in the issue. This issue has no self-contained implementation target or completion test; a contributor would need to choose a concrete piece from “How contributors can help” and define its scope separately.

Written by the indexing model from the issue text.