Technically Coq is not a fully automated automated prover, but leaving that aside: We are definitely not even close. But getting mathematicians acquainted with

Technically Coq is not a fully automated automated prover, but leaving that aside: We are definitely not even close. But getting mathematicians acquainted with HoTT is a good first step, I think. The book itself presents formulations of homotopy theory, set theory, category theory, and a constructive view of the real numbers, all within homotopy type theory, and on top of all this we could likely start building up a corpus of more results from topology, algebra, and analysis.