This paper discusses the formalization in PVS of diverse proofs of the infinitude of primes. These proofs are developed using techniques from various areas of mathematics, including set theory, algebra, analysis, number theory, and topology. The availability of such a variety of proofs is helpful as a didactic resource, aiming to encourage mathematicians working in different areas to adopt interactive theorem provers as one of their everyday tools. The presented collection of formalizations follows the proofs selected by Erdös, Aigner, and Ziegler in their famous work “Proofs from THE BOOK,” namely those based on Fermat numbers, Mersenne numbers and algebraic structures, topological properties, and the analysis of harmonic series. The paper discusses the differences between informal proofs and mechanical formalization, highlighting the usefulness of distinguishing features of PVS to guide and facilitate the presented mechanization.