Have you ever been really bothered by, in that paper you were reading, the proofs that were "left to the reader", the statements that "clearly follow", but clearly were not clear at all? Have you ever wondered that you could just search for a theorem on arXiv, click on it, and it would show all the lemmas it depended on? Have you ever wished your computer algebra system would "understand" the abstract concepts, rather than merely performing computations? The good news is, although there is a long way to go for it to be practical for working mathematicians, the existing theories and technologies of formal verification are already capable of formalizing a large body of modern mathematics. In this talk, I will introduce the building blocks of formal verification, including logical foundations, proof assistants, and expressing mathematics formally in such systems. In particular, I will illustrate the relevant concepts by giving a brief overview of type theories, the Coq proof assistant, and the Flyspeck project that formally verified the 400 years old Kepler's Conjecture on sphere packing. Furthermore, I will discuss common challenges in formalization endeavors. The talk is aimed at a general mathematical audience.