Taking into consideration Calvino's 1967 lecture "Cibernetica e  fantasmi," the article discusses wheter the similarities between mathematics and literature previously noticed when reading Calvino's Six Memos for the Next  Millennium (Lezioni americane) may be extended to include both central characteristics of 21st century mathematics and the mechanization of formal proofs.