So, the trick is that the untyped lambda calculus is not very useful as a mathematical proof, since it has non-halting terms.
Lambda Calculus as a proof system is most useful with types, particularly in terms of the Curry-Howard Isomorphism. Phillip Wadler has a great article outlining this.
The basic idea is that lambda abstraction corresponds to the way that you prove an implication. To write a function of type $A \to B$, you assume you have a value of type $A$, and use it to construct a return value of type $B$.
This is exactly how you prove $A \implies B$: assume that $A$ holds, then use this to prove $B$.
Not every lambda term corresponds to a mathematical proof in the sense we're used to, although each term can be regarded as a proof that its type is inhabited. In particular, to prove anything really useful, you need dependent types, where types are allowed to be indexed by values.
For Church-Numerals, their typed version if $\forall a \ldotp a \to (a \to a) \to a$, which, when interpreted as a proposition, is really boring. It's saying that if something holds, and it implies itself, then that something still holds.
For more information on the various type systems for Lambda Calculi, I'd start with the Lambda Cube.