When I see a statement like that, I just cannot stop myself from pulling the trigger:

Why does Wittgenstein want surveyability? He seems to think that to be capable of the specific use of a theorem which a new proof makes possible we must be able to

reproduceits proof. This is just false, indeed perversely so — without understanding anything about Wiles’ proof of Fermat’s Last Theorem you can use it to rule out the truth of \(a^{17} + b^{17} = c^{17} \) where \(a\), \(b\) and \(c\) are any three integers, even hundreds of digits long — for example I know that \(123456789^{17} + 12233445566778899^{17}\) can’t be equal to \(12345678901234567890^{17}\) without needing to calculate any of the three powers. [Edwin Coleman,The surveyability of long proofs, Foundations of Science,, 14, Issue 1–2, pp 27–43.]