> but if someone thinks that writing incomprehensible but correct proofs is as fine as it gets — it's huge mistake to think so. In the brute force case, it's s

> but if someone thinks that writing incomprehensible but correct proofs is as fine as it gets — it's huge mistake to think so. In the brute force case, it's simply a conceit of mathematicians that algorithms implemented in a programming language are incomprehensible. If our proofs can span hundreds of pages, why not also our programs? Accepting the premise that large algorithms and their results can be used as part of a proof, have you ever proven a program correct by hand? It's almost always tedious and unenlightening.