Abstract: The classical isoperimetric inequality states that in Euclidean space spheres provide unique enclosures of least perimeter for any given volume. In this talk we show how this inequality may be extended to spaces of nonpositive curvature, known as Cartan-Hadamard manifolds, as conjectured by Aubin, Gromov, Burago, and Zalgaller in 1970s and 80s. The proof is based on a comparison formula for total curvature of level sets in Riemannian manifolds, and estimates for the smooth approximation of the signed distance function, via inf-convolution and Reilly type formulas among other techniques. Immediate applications include sharp extensions of Sobolev and Faber-Krahn inequalities to spaces of nonpositive curvature. This is joint work with Joel Spruck.