I'm building a project in this area called Alkahest: https://github.com/alkahest-cas/alkahest. It is a computer algebra system built in Rust that emits corresponding Lean certificates for many of its operations that can be formally verified.

Alkahest is available as a Python library or a Rust crate. It's designed for agent use with good debugging output.

I'm rapidly iterating on it, feel free to send any issues/comments/ideas my way.