Formal Lie theory in characteristic zero

Let be a field of characteristic zero. The intuition is that in this case, a Lie algebra is the same data as a “germ” of a Lie group, or of an algebraic group. This is made precise in the following:

Theorem 1 There is an equivalence of categories between:

1. Cocommutative Hopf algebras over which are generated by a finite number of primitive elements.
2. Finite-dimensional Lie algebras.
3. Infinitesimal formal group schemes over (with finite-dimensional tangent space), i.e. those which are thickenings of one point.
4. Formal group laws (in many variables).

The result about Hopf algebras is a classical result of Milnor and Moore (of which there is a general version applying in characteristic ); the purpose of this post is (mostly) to describe how it follows from general nonsense about group schemes.