Merzlyakov's Theorem states that any positive AE-sentence that is true in the free group has a formal solution. In other words, the existential variables can be replaced by explicit words in the constants and the universal variables.  Despite the logic-oriented terminology of this theorem, its proof falls under the purview of geometric group theory. We will discuss this theorem and its generalisations by Sela and others.