I remember reading somewhere that it takes about a week to convert a page of math into something a proof-assistant like Isabelle or HOL Light would accept. Is this type of conversion something that ...
For example I have read that is agony to give a complete proof of the Jordan curve theorem. Since all statements are meant to be justified by the postulates, where does the difficulty lie?
This question is related to (maybe even the same in intent as) Question 1017, but none of the answers seem to address what I'm looking for. There are a lot of resources available for people who want ...