This is a lot less ad-hoc than whatever CAS's do, but it's also less error prone.

All of the axiomatic transformations applied by a CAS like SymPy should/must be in Lean Mathlib somewhere? If nothing else, a lookup_lean_mathlib_definition(expr, 'path/to/mathlib-v0.0.2') or find_similar(expr, AxiomDB) would be useful.

How do CAS differ from Production Rule Systems? https://en.wikipedia.org/wiki/Production_system_(computer_sc...

CAS > Simplification: https://en.wikipedia.org/wiki/Computer_algebra#Simplificatio...

Rewriting: https://en.wikipedia.org/wiki/Rewriting

Because the rulesets are expected to change, rules engines have functionality to compile rules into a tree or better for performance.

eBPF is not a rules engine, but it does optimize filter sets IIRC?

Are fundamental constants other-valued in any Many Worlds interpretations, or are e, i, and Pi always e, i, and pi with the same relations?

Countability and continuua (in a Hilbert space of degree n, where n is or is not inconstant like the many forms of [quantum discord] entropy and the energy that represents them)

TIL the separable states problem is considered NP-hard, and many models specify independence of observation as necessary.

> In this game, you get own version of the natural numbers, called `mynat`, in an interactive theorem prover called Lean. Your version of the natural numbers satisfies something called the principle of mathematical induction, and a couple of other things too (Peano's axioms).

Such axioms are hard-coded in SymPy, SageMath, and Mathematica but not in Lean Mathlib (which is not optimized for performance)

If there are an infinite number of unitary transformations (as rotations on a Bloch sphere for example), I find it unlikely that we've yet discovered all of the requisite operators and axioms and coded them into any human CAS that exists in present day.