I'm excited about HoTT, too. If anyone has demonstrated a short proof of the four-color map theorem in Coq, that would meet Devlin's criteria for convincing mac

I'm excited about HoTT, too. If anyone has demonstrated a short proof of the four-color map theorem in Coq, that would meet Devlin's criteria for convincing machine-checked proofs. (Check the link you cited; Devlin mentions 1976 and 1994 as key milestones for machine-checked proofs) But HoTT and Coq are both still new, particularly when speaking of mathematics. When they figure out how to make LaTeX produce their textbook in a fully MathML-compatible fashion, then we can talk. :)