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 requires a lot of search and creativity, or is it near-mechanical?



Does formalizing math require search and creativity, or is it near-mechanical?
Formalisation time per page is far from constant. It depends on the material. Sometimes you race through the pages, and at other times you make no progress at all. 


Obstacles to formalisation include 


* gaps or errors in the presentation;
* flights into metamathematical arguments, appeals to global symmetries, etc.;
* unexpected references to major theorems in some other domain of mathematics.


Sometimes, the author just gives up. Kunen's excellent text *Set Theory* contains a fine exposition of the development of constructible sets and the axiom V=L, but his proof that GCH follows from V=L is the briefest sketch, a mere 10 lines. This for a proof that took Gödel two years and arguably triggered a mental breakdown. In other cases, you will find that the hardest part of the proof has been left as an exercise.


You need to study your material carefully to see whether it can be formalised with a reasonable effort.


