The formal semiclassical limit of the 'exact' Hohenberg-Kohn (HK) functional with the one-body density held fixed was introduced in a series of fundamental papers by Seidl (1999), Seidl/Perdew/Levy (1999), Seidl/Gori-Giorgi Savin (2007). The goal of my talk is three-fold
(i) to explain how the Levy-Lieb constrained search definition of the HK functional reduces in the limit to an optimal transport problem [1]
(ii) to discuss the rigorous mathematical theory of the limit problem, including
-- justification of the formal semiclassical limit [1]
-- qualitative theory of OT problems with Coulomb cost, including the question whether ''Kantorovich minimizers'' must be ''Monge minimizers'' (yes for 2 particles, open for N particles, no for infinitely many particles) [1,2]
-- exactly soluble cases (N=2 with radial density; N=infinity) [1, 2]
(iii) to present a natural hierarchy of further approximations of the limit functional related to representability constraints on the pair density which survive in the classical limit [3].

[1] C.Cotar, G.F., C.Klueppelberg, arxiv.org/abs/1104.0603, 2011; Comm. Pure Appl. Math. 66, 548-599, 2013
[2] C.Cotar, G.F., B.Pass, http://arxiv.org/abs/1307.6540, 2013
[3] G.F., Ch.Mendl, B.Pass, C.Cotar, C.Klueppelberg, to appear in J. Chem. Phys., http://arxiv.org/abs/1304.0679