1. Checking a series of logical statements (a proof) is obviously decidable; it's a mere exercise in syntactic manipulation. This is exactly what Isabelle/HOL/Coq/Agda/etc. do.
2. Yes, the validity of theorems is undecidable. But even if that's what the quote was talking about (it's not, read the context), confirming truth (soundness) is very much something computers are capable of. Correctly deciding truth or falsity (soundness + completeness) is what is not possible in every case.
2. Yes, the validity of theorems is undecidable. But even if that's what the quote was talking about (it's not, read the context), confirming truth (soundness) is very much something computers are capable of. Correctly deciding truth or falsity (soundness + completeness) is what is not possible in every case.