raph: I'm not surprised by the quality of the responses you have received to your recent musings on web-based proof systems: this is a difficult area, both technically and philosophically and as a perfect outsider you have talked about the topic intelligently and persuasively. I think that there is every chance that your web-based proof-exchange protocols will prove to be successful and important.

Various comments:

• Solovay's comment about strength of ZFC and HOL, while true, may be misleading. I am not familiar with HOL, but I believe that it is based on the Girard-Reynolds polymorphic lambda calculus: the embedding of such a calculus into ZFC is not straightforward; see John Reynold's classic paper, `polymorphism is not set-theoretic'.
• A poster suggested thinking about translations between proof representations using category theoretic formalisms. I think this is probably a good idea. The poster also mentioned topos theory in this connection: this is possibly more work than is necessary for your purposes.
• I suggested second-order arithmetic as a good basis formalism: I think it makes life easy if most people use a single formalism, and the extra strength of ZFC is almost never necessary (also one can just add axioms to SOA to obtain equivalent strength to ZFC).