I don't think it's as difficult as you think it is. It's still a lot of work to implement mind you, but not nearly impossible. I talked about Mathlib [0] in a r

I don't think it's as difficult as you think it is. It's still a lot of work to implement mind you, but not nearly impossible. I talked about Mathlib [0] in a reply to the grandparent comment, which is a library of mathematical theorems and proofs that has a big community effort behind it. The language they use to state theorems would help a lot in making mathematics machine-readable enough for a computer algebra system to be able to make sense of it. I'm hoping to build a prototype for this sometime in Julia's `Symbolics.jl` CAS. It would be just a simple proof of concept to implement derivative and integral rules from Mathlib or some custom maths library, and get them into the CAS. Symbolics.jl seems to be a perfect fit for this since it's made to be extensible, and Julia's metaprogramming would be a welcome addition as well. Either way, I would love to see this become part of the CAS ecosystem. [0] https://leanprover-community.github.io/ https://leanprover-community.github.io/