computer algebra system (CAS) is inadequate for the Physics Derivation Graph (PDG)

I'm beginning to appreciate that a computer algebra system (CAS) is not sufficient for the Physics Derivation Graph (PDG). The evidence of this is that the variables I'm defining can be real or complex; that is not distinguished by the computer algebra system.

The simple story of starting with

a = b

and then adding 2 to both sides to get

a+2 = b+2

is appropriate for a computer algebra system. But if "a" is a matrix then the operation is invalid. The only way to distinguish "scalar a" from "vector a" from "matrix a" is to specify the difference. [SymPy does have support for predicates -- https://docs.sympy.org/latest/guides/assumptions.html#predicates .]

In the Physics Derivation Graph I want to be more specific about the possible values of a and b. Even for non-physics derivations like the Euler equations, there are assumptions about the possible values of each variable.

I don't know Lean, but I also don't know the foundational concepts of theorems and proofs.
Is a step a theorem?
Is a derivation a theorem?
The role of inference rules in steps in derivations does not map to anything in a theorem.