Symbolic rule-learning engines: derivations as searchable state spaces

A derivation is a program. Its state is a string of symbols; its instructions are rewrite rules that turn one legal string into another; and the derivation itself is the trace — the sequence of states the rules walk you through. Once you see derivations that way, a whole family of systems comes into focus: engines that apply symbolic rewrite rules, engines that search for the right sequence of rules, and engines that try to learn the rules themselves. This page is the map of those engines, grounded in the smallest one that actually runs.

The substrate: rules in, derivation out

Strip everything down and a symbolic engine is this: a set of rewrite rules, and a loop that applies one until none fire. Differentiation is the cleanest example — the state is an expression carrying $d/dx$ nodes, the rules are the differentiation laws, and the derivation is the trace of pushing those operators inward.

# A derivation is a sequence of states connected by named rewrite rules.
# Here the state is an expression with d/dx nodes; the rules are the
# differentiation laws; the derivation is what you get by applying one rule
# at a time until no d/dx node remains. The rules ARE the program.

RULES = []
def rule(name):
    def deco(f): RULES.append((name, f)); return f
    return deco

@rule("d/dx[x] = 1")
def r_x(e):
    if is_op(e,'d') and e[1]==('x',): return ('c',1)
@rule("sum rule")
def r_sum(e):
    if is_op(e,'d') and is_op(e[1],'+'): return ('+',('d',e[1][1]),('d',e[1][2]))
@rule("product rule")
def r_prod(e):
    if is_op(e,'d') and is_op(e[1],'*'):
        u,v=e[1][1],e[1][2]; return ('+',('*',('d',u),v),('*',u,('d',v)))
@rule("power rule")
def r_pow(e):
    if is_op(e,'d') and is_op(e[1],'pow') and e[1][1]==('x',):
        n=e[1][2]; return ('*',('c',n),('pow',('x',),n-1))
# ... (const rule, sin rule, etc.)

def apply_once(e):                       # leftmost-outermost rule that fires
    for name,f in RULES:
        r=f(e)
        if r is not None: return r,name
    if isinstance(e,tuple):              # otherwise recurse into subexpressions
        for i in range(1,len(e)):
            if isinstance(e[i],tuple):
                sub=apply_once(e[i])
                if sub: return e[:i]+(sub[0],)+e[i+1:], sub[1]
    return None

expr=('d', ('+', ('pow',('x',),3), ('*',('pow',('x',),2),('sin',('x',)))))
while (out:=apply_once(expr)):
    expr,name=out; print(f"[{name}]  {show(expr)}")

start:  d/dx[x^3 + (x^2)·sin(x)]
[sum rule       ]  d/dx[x^3] + d/dx[(x^2)·sin(x)]
[power rule     ]  3·x^2 + d/dx[(x^2)·sin(x)]
[product rule   ]  3·x^2 + (d/dx[x^2])·sin(x) + (x^2)·(d/dx[sin(x)])
[power rule     ]  3·x^2 + (2·x^1)·sin(x) + (x^2)·(d/dx[sin(x)])
[d/dx[sin]=cos  ]  3·x^2 + (2·x^1)·sin(x) + (x^2)·cos(x)
-> 5 rule applications; no d/dx left, done.

That output is a derivation in the most literal sense: each line is one legal move, tagged with the rule that fired. It is also, exactly, the step format the DerivationWalker on this site already renders — its move field is the name of the rule. The only difference is that the DerivationWalker's steps are currently hand-authored; here they are generated by the rules. The rules are the program; the derivation is its output. That is the substrate every engine below sits on.

Where the difficulty — and the learning — actually enters

Differentiation needs no intelligence: at each state exactly one rule fires (the system is confluent and terminating), so applying rules blindly reaches the answer. Real derivations aren't like that. At a typical proof state many rules apply, most lead nowhere, and you are searching for a path to a goal you've specified in advance. So a derivation is not a forward random walk — it is goal-directed search over a branching tree of rewrites, and the three things you might learn correspond to three places the difficulty lives:

• Which rule to apply next (a policy over moves) — to prune a branching factor that otherwise explodes.
• How promising a state is (a value function) — to know whether a partial derivation is heading somewhere, the long-horizon credit-assignment problem.
• What the rules even are (rule induction) — to discover the rewrite laws, or new identities, from examples rather than being handed them.

The map of engines

Organized by what's given versus what's learned:

A few of these are worth pinning down, because the others are variations on them:

• Lean + Mathlib is the existence proof that the whole idea works for mathematics: a million-plus lines of derivations as machine-checkable move-sequences. The "dataset of legal walks" is real, for math.
• AlphaProof (DeepMind, 2024) and AlphaGeometry (Nature, 2024) are the "learn the transition policy" systems made good — a learned policy over moves plus tree search, reaching IMO-medal level. AlphaGeometry works precisely because Euclidean geometry's moves are fully formalizable; that caveat matters below.
• The Ramanujan Machine (Nature, 2021) is the one that does what you'd actually call "finding unknown patterns in symbolic structure": it searched the space of continued fractions and conjectured new formulas for $\pi$, $e$, and $\zeta (3)$ — which lands right back on the continued-fraction thread elsewhere on this site.
• Equality saturation / e-graphs (the egg library) is the engineering answer to "the rewrite space explodes": represent all equivalent rewrites of an expression in one shared graph, saturate, then extract the best. The state space, made a data structure.

Why physics is the hard case

Everything above is mathematics. Physics resists it, for two concrete reasons.

• Physics derivations aren't a clean rewrite system. They interleave syntactic rewrites with semantic moves: drop a term because it's small, choose an ansatz, change gauge, take a limit, argue by dimensional analysis. Those aren't mechanical rule applications — they're where the physics and the taste live. The "legal move set" is partly informal, which is exactly why AlphaGeometry's formalizable-domain success doesn't transfer for free to general physics.
• The dataset doesn't exist in machine-readable form. Physics derivations live in papers and textbooks as prose plus LaTeX, not as typed sequences of named rewrite steps. Building that corpus — and finding the right abstractions, the level at which a derivation in TDDFT and one in circuit theory are the same derivation — is the undone, valuable work.

That second point is not hypothetical here. The recurring move across this site has been finding the same derivation wearing different clothes: the Gaussian product theorem is the parallel axis theorem; Lanczos is orthogonal polynomials is Gauss quadrature is Padé is the moment problem, one derivation in five costumes. Those cross-domain identifications are precisely the patterns a physics rule-learning engine would aim to surface automatically — and the claims system plus the DerivationWalker are the beginnings of the corpus and the renderer it would need.

What it would take

The grand version — "learn new physics from the symbolic structure of known physics" — is a research program, not a build. Current systems prove statements you hand them (AlphaProof), or conjecture identities in narrow, formalizable domains (Ramanujan Machine, AlphaGeometry), or fit equations to data (symbolic regression). None yet discovers new physical theory from a corpus of derivations, because the corpus isn't formalized and the moves aren't all syntactic. The tractable first step is small: a rewrite engine like the one above, with rules specified as data, generating derivations into the DerivationWalker — and a pattern-miner over the resulting rule-sequences looking for shared motifs across derivations. On a small corpus you'd see motifs like "complete the square → exponentiate" recur across the Gaussian product theorem and the Moshinsky transform — the abstraction emerging from data instead of being spotted by hand. That's the seed of a meta-derivation engine: not the oracle, but the substrate plus a magnifying glass.

Related on this site

• Lanczos ↔ continued fractions — a worked example of "the same derivation in many guises," the kind of pattern such an engine would target.
• Casida Hermitian rewrite (DerivationWalker) — derivation steps as named rewrite moves, hand-authored for now.
• Claims — atomic, citeable, relation-linked facts: the proto-corpus a rule-learner would mine.
• Self-learning Monte Carlo — a different "learn a cheap surrogate, keep the truth exact" pattern, in sampling rather than symbolics.

References

• Baader, F. & Nipkow, T. (1998). Term Rewriting and All That. Cambridge.
• Polu, S. & Sutskever, I. (2020). Generative language modeling for automated theorem proving. arXiv:2009.03393 (GPT-f).
• Lample, G. et al. (2022). HyperTree Proof Search for Neural Theorem Proving. NeurIPS.
• Trinh, T. et al. (2024). Solving olympiad geometry without human demonstrations. Nature (AlphaGeometry).
• DeepMind (2024). AI achieves silver-medal standard solving IMO problems (AlphaProof / AlphaGeometry 2).
• Willsey, M. et al. (2021). egg: Fast and Extensible Equality Saturation. POPL.
• Raayoni, G. et al. (2021). Generating conjectures on fundamental constants with the Ramanujan Machine. Nature, 590, 67–73.
• Udrescu, S.-M. & Tegmark, M. (2020). AI Feynman: a physics-inspired method for symbolic regression. Science Advances.
• Cropper, A. & Dumančić, S. (2022). Inductive Logic Programming at 30. JAIR.