Faltings's original proof used the known reduction to a case of the Tate conjecture, and a number of tools from algebraic geometry, including the theory of Néron models. A very different proof, based on diophantine approximation, was found by Vojta (1991). A more elementary variant of Vojta's proof was given by Bombieri (1990).
Faltings's 1983 paper had as consequences a number of statements which had previously been conjectured:
The reduction of the Mordell conjecture to the Shafarevich conjecture was due to A. N. Paršin (1971). A sample application of Faltings's theorem is to a weak form of Fermat's Last Theorem: for any fixed n > 4 there are at most finitely many primitive integer solutions to an + bn = cn, since for such n the curve xn + yn = 1 has genus greater than 1.
Because of the Mordell–Weil theorem, Faltings's theorem can be reformulated as a statement about the intersection of a curve C with a finitely generated subgroup Γ of an abelian variety A. Generalizing by replacing C by an arbitrary subvariety of A and Γ by an arbitrary finite-rank subgroup of A leads to the Mordell–Lang conjecture, which was proved by Faltings (1991, 1994).