One-body localization in disordered quantum systems, such as described by the Anderson model, is mathematically well understood. However, in more realistic physical systems one should understand localization as a many-body effect. The latter is still a widely open problem, even in physics. We will describe ways in which many-body localization can be characterized and discuss one or two simple models for which it can be rigorously proven.