In mathematics, a formal group law is (roughly speaking) the formal power series analogue of a Lie group. Given a Lie group G and a chart around its identity element e, such that e is given coordinates (0, 0, ..., 0), the group operation in G is some function

F(x₁,x₂, ..., x_n,y₁,y₂, ..., y_n)

where n is the dimension of G, taking values in Rⁿ. Suppose we take the power series expansion of F (formal Taylor series) and look at the identities it should satisfy on the basis of the group axioms - for example the associative law (for the inverse operation take also an expansion of the inverse mapping I). Then we can turn these power series identities into a fresh definition, of a formal group law (often just formal group) in n variables.

The nature of a 'formal group' is not therefore as a group in the set-theoretic sense: it is more like the bare definition

F(x,y) = x + y + xy

that comes from thinking about multiplication near 1. It is not either a group object in the sense of category theory (as a Lie group is). It does provide an actual group when the variable x is given values in a ring such as

R[t]/(t^k), for k = 1, 2, ...

for which convergence is guaranteed since t has been forced to be nilpotent. There is an abstract sense in which the formal group here is an inverse limit of group schemes; or a functor from artinian R-algebras to groups.

There was early work on formal groups of elliptic curves by Lutz; the idea later became important in the classification of abelian varieties in non-zero characteristic. The theory was also much used in algebraic topology in the 1960s, after it was seen that it played a role in homology theory. To be precise, cobordism theory needed the universal one-dimensional formal group over Z, the existence of which had been proved by Lazard.