Anyway this is one of the hottest research topics in CS. I know we keep seeing deep learning papers all the time, one might think this is the only thing happening in CS world. Currently it is nowhere near easy to formalize a complex enough theorem in a system like this. Good news is there is a large chunk of certain theories (like homotopy theory) already formalized for you, so you can go ahead and use them as libraries.
The biggest challenge is mathematics is written for humans, it is not meant to be formal. When you formalize theorems you start proving smallest shit you'd never have thought that would need a proof. You even need to prove things like what it means x == y and that for all x, x==x. There is no AI involved in this currently, so it's a very manual, intellectually complicated and long process. These systems have a proof finder built into them which performs a tree search with heuristic to help you, this usually makes manual proofs easier, but usually only marginally easier and you still have to micromanage your proofs.
Keywords you can search: automated theorem proving, dependent type theory and homotopy type theory.