I don't think SymPy has abstract Function attributes to reason about, but it does have limited reasoning about number classes given e.g. `x = Symbol('x', real=T

I don't think SymPy has abstract Function attributes to reason about, but it does have limited reasoning about number classes given e.g. `x = Symbol('x', real=True)` SymPy docs > Writing Custom Functions > Easy Cases: Fully Symbolic or Fully Evaluated: https://docs.sympy.org/latest/guides/custom-functions.html#writing-custom-functions https://docs.sympy.org/latest/guides/custom-functions.html#w... If there is some sort of e.g. geometric correspondence, it could be possible for a Church-Turing classical computer to compute quantum functions (that return wave functions) that a Church-Turing-Deutsch quantum computer can compute; but otherwise Lean can't compute most quantum circuits either.