This is Erdős’s proof of the divergence of the sum of prime reciprocals, using the Mizar system [2], [3], as reported in “Proofs from THE BOOK” [1].