This is not as easy as some comments here imply. Basically, there are 3 popular languages used for this in a academia and the industry: Coq, Isabelle/HOL and Ag

This is not as easy as some comments here imply. Basically, there are 3 popular languages used for this in a academia and the industry: Coq, Isabelle/HOL and Agda. They're all extremely different languages doing different things (but their end goal is the same: formalizing and automating proving). Coq and Agda are intuitionistic by design, you need assume lem to be classical. Agda has a Haskell heritage so it's purely functional other two are more "procedural". Coq has 2 languages built into it, a tactic language and a language go write types in. 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.