Check out https://github.com/leanprover-community/mathlib . Sure, it's not really a CAS but CAS algorithms could be added to it where applicable, since Lean is a constructive system and can thus express formally verified computations.
The existence of https://github.com/robertylewis/mathematica makes me think it's more likely to go in the other direction, where you treat powerful tools as untrusted oracles which produce certificates that Lean then verifies.
Sure that's possible, but "untrusted oracles" are only useful if they provide easily-verified certificates. Some CAS problems are amenable to that approach, but not all. There's no difference in this case between Mma and, e.g. an external SAT/SMT solver.
