Does formalizing math require search and creativity, or is it near-mechanical? 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?
 A: I'm not an expert (I've played around with HOL a few times, but never fully formalized an interesting theorem), but my experience was that it's similar to writing up a technical proof after you've worked out in your head how to do it: most of the process is pretty directed and you're just filling in details, but you often have to pause at the start of a step to think about the best approach (which requires a small amount of creativity), and every so often you encounter a serious difficulty that requires real thought and creativity to get through (on the scale of patching a small hole in the proof you mostly know, not on the scale of coming up with a new proof in the first place).
A: Like Henry, I am not an expert---although I've played around with formal proof assistants.  
First, one has to take into account if the background material is already formalized.  This can make a big difference.  If it is not already formalized then you may need to select a different proof that is more computational and avoids tricks that venture into other territory.  (If the proof you are formalizing is fairly new, you may need to do that work yourself which obviously takes time and creativity.)  Alternately, one needs to formalize this background material (which can be satisfying, but also takes time).
Second, it matters if you are going for building a beautiful library of math or just trying to hack together some proof until the computer says "proved".  In the former case, you may actually spend a few weeks thinking about how you want to set up the whole structure.  (As an example, would you define a ring as an Abelian group with multiplication, or would you define it from scratch?  If you define it as an Abelian group, then you could also use all the theorems you proved for Abelian groups for rings as well.)
Last, it takes some time to get into the swing of using a proof assistant, but after that, it is fairly mechanical.  Nonetheless, there will be a number of times when you think to yourself "this is obvious, but I guess the computer doesn't know that".  Then you have to figure out how to convince the computer that it is true, usually by breaking the proof into some trivial logic.  However, as with all things, with experience this happens less and less.
I am sorry I can't give you a rate like "one day per page", mostly from my lack of experience.
A: This may depend sensitively on the subject area.  My impression (or perhaps my prejudice) is that proofs in certain areas, like geometric topology, are much farther from being formalized than proofs in most other areas of mathematics.
A: 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.
