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

[Rafael-SOWNet]

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
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.

---

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: 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:

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),
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
and the accepted syntax written down in
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.

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) 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)
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 and
#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,
#338,
#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 and
#552 already ask for. This collides
head-on with #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).

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, 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,
#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.

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).
• 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,
  #500).

Major deliverables. The polynomial layer; a specified canonicaliser; the pattern-matching engine;
API and behaviour consistency sweeps; documentation of every public surface
(#585); the measured corpus.

Example issues. #185 (polynomial
simplifier with replacements), #205 (surds),
#204 (roots vs fractional powers),
#203 (collapse must collapse),
#176,
#740,
#224 (caching linear children),
#392 (FastString),
#381 (characteristic polynomial),
#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
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 (collect intermediate
pattern replacements), #195 (aggressive
replacement), #322,
#327 (Piecewise patterns),
#415 (simplify intervals),
#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 (groups, rings, fields) and
  #510 (generic math structure) to be its
  first real inhabitants.
• Statements as data: hypotheses, conclusion, quantifiers
  (#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 and
#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).
• 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 corner cases;
#357 (dependency reduction) as a planning
step; #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) —
  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 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);
more integral solvers (#233); more limit
solvers (#231); set, vector and matrix
equations (#95);
#105 (cross and dot on arbitrary entities);
symbolic linear algebra decompositions; a Pythagorean-triple solver
(#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-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 (SymPy
parity) and #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: <easy> up-for-grabs, <medium> up-for-grabs, <hard> 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.
3. Add a regression test for an open bug that is still open — the test alone is a contribution.
4. Write XML documentation with a worked example for one MathS member
   (#585).
5. Fix a ToString/Latexise precedence or parenthesisation case and add the round-trip test.
6. Make commit numbers in version_performance_control.md link to their commits
   (#167).
7. Add decimal and mixed-fraction output options (#159).
8. Extend the Syntax.md documentation to cover a grammar feature it currently omits.
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).
11. Improve one exception message so it names the offending sub-expression.
12. Add an F# wrapper for a C# API that lacks one.
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.

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

16. Implement one classical algorithm behind the existing tracker: a logarithmic equation solver
    (#246), exponential and logarithmic
    equations (#214).
17. Surd simplification (#205) — and
    decide and document the roots-versus-fractional-powers convention
    (#204) while you are there.
18. Make Entity serializable (#323) —
    a v6/v8 prerequisite hiding in an old issue.
19. Cache LinearChildren (#224).
20. FastString instead of string for ToString (#392).
21. N-ary operators with variables (#248).
22. Simplification patterns for Piecewise (#327)
    and syntax for it (#326).
23. Interval simplification (#415).
24. Subset operator (#325) and extended
    ConditionalSet definitions (#330).
25. Apply a transformation to every element of a set (#322).
26. Characteristic polynomial (#381).
27. Compile matrices (#526).
28. Inverse and derivative for factorial and gamma (#171).
29. Differentiation with respect to functions (#230).
30. Complex infinity, properly (#217).
31. Parametric solutions (#212).
32. Trigonometric equations expressed via arc functions (#270).
33. Single-threaded timeouts (#373) — and
    the budget object v4.0 needs is the same object.
34. A performance reporter (#500) and
    inter-version benchmarking on key commits (#529).
35. Coverage for F#, Interactive and C++ (#397).
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.
37. Collect intermediate pattern replacements when simplifying
    (#28) — the smallest real step toward
    explainability, open since the early days.
38. Package AngouriMath.Terminal as a dotnet tool (#627).
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).
41. Mine another open-source CAS's issue tracker for cases we get wrong
    (#180).
42. Extend ToSympy to every node with a SymPy equivalent, with round-trip tests
    (#717).

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.
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,
    #231).
46. Gröbner bases and a real system-of-equations solver.
47. Quantifier elimination (CAD or a modern alternative) — the missing machinery behind most
    inequality work and behind #225.
48. Analytical ODE solvers (#241).
49. The step recorder with reversible trees (#273).
50. The rule registry: turn the pattern set into enumerable, attributable data without regressing
    Simplify performance. A Design document first.
51. An e-graph / equality-saturation prototype over Entity, with honest memory measurements on
    realistic input and a recommendation either way.
52. A pluggable cost model, with at least three implementations that visibly disagree.
53. Groups, rings and fields as first-class (#440),
    building on #510.
54. Functions and lambdas as entities (#286,
    #495).
55. Quantifiers (#225).
56. Non-kernel functions and assembly-discovered types
    (#321,
    #338) — the first real extensibility
    seam, and the ancestor of the v9.0 package format.
57. AOT-supported Linq compilation (#363).
58. Interval arithmetic with guaranteed bounds.
59. Arbitrary-precision special functions with documented branch cuts, checked against DLMF at the
    points where conventions disagree.
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).
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.
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).
73. Track SymPy, Maxima and SageMath releases for algorithms and behaviour worth matching
    (#717).
74. Document conventions we have chosen and never wrote down — branch cuts, mod sign, ordering, the
    arsinh spelling and why.
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.
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.

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,
    #552 and every extensibility decision
    above from being quietly undone.
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,
    #500).

---

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.

[Happypig375]

LGTM 🦆

Remember to keep benchmarking to ensure that we don't lose on speed and memory on popular use cases, and keep testing to ensure bug-free code

Also make sure that any reflection, if used, is fine with assembly trimming by e.g. NativeAOT

[darkfader]

And maybe use multiple libraries to split common-use vs edge cases

[WhiteBlackGoose]

☠️

[Rafael-SOWNet]

Thanks both — folded into the body rather than left to be re-derived from the thread.

@Happypig375's three points are structural now rather than implied:

• Trimming / NativeAOT is stated as a constraint on extensibility, because the vision as written had a genuine collision in it that I had not named: Look up for types in the assembly to be able to parse them from a string? #338 (looking types up in the assembly so they can be parsed from a string) and any v9.0 plugin loader are inherently reflective, while AOT-supported Linq compilation #363 and Unity to be supported #552 (Unity) need trimming and AOT. Resolution direction written down — source generators and explicit registration in preference to runtime type lookup; where a reflective path is unavoidable, keep it opt-in, off the hot path, trimmer-annotated, and covered by a test that publishes trimmed and actually runs. v9.0 knowledge packs now have to declare their contents statically instead of being discovered by scanning.
• Benchmarking and testing are promoted out of the roadmap into a new Packaging, and what must never regress section, so they read as conditions on every tier rather than as items someone schedules once. The fast path has to stay bypassable: a rewrite graph, planner or knowledge-graph lookup that cannot be skipped for the easy case is a design error, not a performance to-do.

@darkfader's split is in that same section: the layer boundaries need matching distribution boundaries, so that someone who wants to parse and simplify never downloads a planner or an SMT bridge. That extends the kernel / FSharp / Interactive / Terminal / CPP / Experimental pattern we already ship rather than inventing one — with the cost named honestly, since every boundary widens the version matrix and the CI time, and published package boundaries are close to immovable, so they want deciding early rather than after v2.0 adds anything large.

Three new contributor items (78–80): a Design document for the package split, a trimming + NativeAOT smoke test in CI, and explicitly named popular-use-case benchmarks (parse, Simplify, Solve, Differentiate, time and allocation) with a regression threshold wired into CI rather than left to review.

[Rafael-SOWNet]

Opened #816 as a first, deliberately small piece of the rewrite engine tier — the layer boundary rather than the equality saturation.

What it adds is a way for a mathematical operation to be a value: Transformation carries a name, what it claims about its output, and how well justified that claim is; RewriteRuleSet/RewriteRules make the shipped rewrite groups named, attributed and enumerable. Simplify, Expand, Factorize, Differentiate, Integrate and Limit are now adapters over it, with the algorithms underneath untouched — two of them (Factorize, and the SimplifyChildren pass every stage of the simplifier runs) genuinely composed out of the registry rather than naming their own rules.

Three things from the design principles above are load-bearing in it and worth arguing with:

• Relation before soundness. "Sound" is only a statement about some relation, and a derivative is not another way of writing its integrand — so a transformation says Equivalence or Derivation first. Without that, the tier means nothing and the property test that subtracts output from input gets pointed at operations it says nothing about.
• The tier is declared, not checked. Every shipped rule set is SoundUnderAssumptions and a test holds it there. That is honest rather than useful, and it is the shape §7 (Formalizable) needs if a later layer is ever going to reconstruct a justification.
• The fast path survived as a path. Measured against master on the CommonFunctionsInterVersion expressions: timing ranges overlap, allocation identical or slightly lower. No behavioural change; 5707 tests and 25/25 CI green.

Explicitly not in it, because forcing them in would have damaged the design: Solve (it consumes a goal and produces a solution set — it belongs in the v4.0 tactic layer, and Entity.Set being an Entity means it would type-check here, which is the reason to keep it out); and any inverse machinery, since Expand/Factor are not inverses.

Next two pieces, in order:

1. Register the remaining 16 rule sets Simplificator uses and route it through the registry. Mechanical, but it is what makes the next item tell the truth.
2. Add a way to collect intermediate pattern replacements when simplifying #28 on top of that — a derivation recorder capturing each rewrite as (rule set, before, after), behind a scope so it costs nothing when off. That gets Add a way to collect intermediate pattern replacements when simplifying #28 at rule-set attribution rather than the per-rule attribution its example shows; the finer grain needs the Design document that item 50 asks for, since splitting each switch case into an object trades one dispatch per node for one delegate call per rule per node on the hottest path there is.