[fdej]

There is an algorithm by Richardson to prove equality of real and complex numbers composed from exponentials and logarithms. (It doesn't have a complete proof of correctness, but it never returns a wrong result: it will loop forever iff it encounters a counterexample to Schanuel's conjecture.)

It can also be extended to higher transcendental functions, but it gets harder to guarantee termination.

I have a library for exact reals/complexes with an incomplete implementation of Richardson's algorithm: https://fredrikj.net/calcium/