4 ms·

The proof included with the proof assistant Isabelle is a lot shorter and much easier to read than the Cow proof (in my opinion): https://www.cl.cam.ac.uk/rese

• archgoon 8y ago
  That is indeed far easier to read and understand. :)
• Fede_V 8y ago
  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 :)