Modern society is now being increasingly computerized. Computer-related failures could result in severe economic loss. Mechanized theorem proving is an approach to ensuring stricter correctness, and hence high trustworthiness. First, the logical foundations and key technologies of mechanized theorem proving are discussed. Specifically, first-order logic and resolution-based technology, natural deduction and Curry-Howard correspondence, three logics of programming including first-order programming logic and its variant, FloydHoare logic, and logic for computable functions, hardware verification technology based on higher-order logic, and program constructions and refinement are analyzed, as well as the relationship and evolvement between them. Then key design features of the mainstream proof assistants are compared, and the development and implementation of several representative provers are discussed. Next their applications in the fields of mathematics, compiler verification, operating-system microkernel verification, and circuit design verification are analyzed. Finally, mechanized theorem proving is summarized and challenges and future research directions are put forward.