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.

automating entry of derivations into the Physics Derivation Graph website

What would it take to integrate support for symbol detection and conversion to SymPy for a single step in a derivation?

1. user provides initial expression in Latex to web UI.
2. computer parses symbols and operators from Latex
3. computer searches Physics Derivation Graph database of symbols and operators to find candidate symbols
4. computer provides candidate symbols to user and prompts, "which of the following symbols were you referring to?"
5. computer parses expression to SymPy, returns AST to user, and prompts, "is this the AST you meant?"
6. if yes, continue; if no, go back to step 1 or provide corrections to AST.
7. user provides next expression in Latex
8. computer parses symbols and operators from Latex
9. if symbols match symbols used in this derivation, then associate with those; otherwise 
10. computer searches Physics Derivation Graph database of symbols and operators to find candidate symbols
11. if computer had to search PDG database, then computer provides candidate symbols to user and prompts, "which of the following symbols were you referring to?"
12. computer parses expression from step 7 to SymPy, returns AST to user, and prompts, "is this the AST you meant?"
13. computer uses brute force to check every inference rule using a CAS against the provided expressions to "guess" the inference rule. 
14. if valid inference rule is found, continue to next expression; if no valid inference rule is found, prompt user to provide inference rule.
15. Given the inference rule and associated expressions, use the CAS to verify the step.

use of the Physics Derivation Graph is driven by incentives for individuals

Semantic tagging of documents has the potential of enriching the reader's experience because content is easier to search. The burden of work is on the document author to provide the right tags. Worse, the document author has to find tags that are common to uses in other documents -- consistency of tags is necessary for search. This extra work of 1) tagging and 2) using consistent tags are reasons semantic enrichment hasn't become mainstream. 

The Physics Derivation Graph faces a similar challenge. If the Physics Derivation Graph relies on using appropriately annotated symbols (effectively equivalent to a subset of semantic tags), then the PDG has the same burdens of work on individual authors. 

The incentive for the individual researcher authoring a paper to use the Physics Derivation Graph is when there's integration with a computer algebra system that can check the correctness of steps. Then the author benefits from immediate feedback before sharing with others for review.

Annotating symbols probably isn't sufficient to motivate the work, but integration with a computer algebra system could provide incentive. Currently, the use of a computer algebra system requires detailed steps to be specified by the author. 

There are ways to partially automate both symbol annotation and specifying steps. For symbol annotation, the computer could guess from context which symbols are being used. In a similar reliance on context, the user could provide leaps in specifying a derivation that the computer then tries to fill in with the detailed steps.

Sage as a candidate Computer Algebra System for the Physics Derivation Graph

I was excited to use Sage's online notebook interface to see whether it could handle the variety of expressions and inference rules in the Physics Derivation Graph.

I found a few unexpected behaviors. There's good support for many of the inference rules. When I tried to apply Sage to more advanced uses, either I don't understand the math well enough, or support in Sage doesn't exist.

Expectation value doesn't render Latex

Expectation values are used in the variance relation identity. I was impressed by the ability of Sage to use Expectation value from SymPy.
x=var('x')
from sympy.stats import E # expectation value
expr1=E((x-E(x))^2)==E(x^2)-(E(x))^2
expr2=E(x^2-2*x*E(x)+E(x)^2)==E(x^2)-(E(x))^2
print(bool(expr1.lhs() == expr2.lhs()))
expr3=E(x^2)-2*E(x)*E(x)+E(x)^2==E(x^2)-(E(x))^2
print(bool(expr3.lhs() == expr2.lhs()))

True

True

However, I wasn't able to display the content in LaTeX:

print(latex(expr3))

0 == 0

This is unfortunate but not a blocker

Real Part of Expression isn't what I was expecting

Sage doesn't produce the output I expected from .real_part() 

forget()

x=var('x')

assume(x,'real')

this=cos(x) + I*sin(x)

this.real_part()

cos(real_part(x))*cosh(imag_part(x)) - cos(real_part(x))*sinh(imag_part(x))

What I was looking for was that this.real_part() would return cos(x); similarly this.imag_part() should return sin(x).

Symbolic Levi-Civita not supported in Sage?

A Levi-Civita operator can be defined

levicivita = SymmetricGroup(3)

levicivita([1,2,3]).sign()

1

However, I can't use symbols as arguments

forget()

h,j,k=var('h,j,k')

assume(h,'integer')

assume(j,'integer')

assume(k,'integer')

levicivita = SymmetricGroup(3)

levicivita([j,k,m]).sign()

Invalid permutation vector: [h,j, k]

Del (aka Nabla) lacks symbolic support in Sage?

Symbolic cross-products work as desired
h,j,k=var('h,j,k')
m,n,p=var('m,n,p')
E = vector(SR, [h,j,k])
F = vector(SR, [m,n,p])
print(E.cross_product(F))
(-k*n + j*p, k*m - h*p, -j*m + h*n)

Other vector calculus operations appear to lack support for symbolic manipulation
https://en.wikipedia.org/wiki/Del#Gradient
https://en.wikipedia.org/wiki/Del#Divergence
https://en.wikipedia.org/wiki/Del#Curl

I don't quite understand what's being done with the following:
forget()
V = VectorSpace(SR,3)
h,j,k=var('h,j,k')
m,n,p=var('m,n,p')
E = vector(SR, [h,j,k])
print(E.curl([1,2,3]))
print(E.div([1,2,3]))
(0, -1, 1)
1