Thanks, yes, I meant clopen subsets. Edited to correct

Thanks @Marguax. Can I check I follow? $O_{G,e}$ is the stalk at $e$ of the sheaf of analytic functions on $G$; to say that $F$ is pro-represented by the completion of $O_{G,e}$ w.r.t. its maximal ideal $I$ is to say that $F$ is a filtered colimit of representables, indexed by the cofiltered diagram of Weil algebras $n \mapsto O_{G,e}/(I^n)$. Thus $F$ can be seen as a cogroup in $\mathrm{Pro}(\mathrm{Weil})$. Taking cofiltered limits now sends coproduct to the (completed) tensor product of topological algebras, so finally we get a commutative Hopf algebra. Is that right?

Thanks, this is just the sort of thing I was looking for. I had the feeling that one should use something else than an actual formal group law. I was aware of the two dual Hopf algebras arising from O(G) and U(G) but not how to construct them directly from G. I had a few questions which I've appended to Marguax's comments above.

Thanks, Peter. You're right that (1) and (2) are not in correspondence in quite the form I stated. Have edited. As to your other comment, that is illuminating; really what is happening is that the equivalence between the categories of Lie algebras and formal group laws is only canonically defined in the direction from the latter to the former; the converse requires the axiom of choice (a choice of basis for each Lie algebra).