Hacker News Reader

The proof included with the proof assistant Isabelle is a lot shorter and much easier to read than the Cow proof (in my opinion):

Interestingly, Isabelle is the director of the INRIA institute in Paris where a lot of coq is developed. I wonder if it's named after her :)

That is indeed far easier to read and understand. :)