Mathematical proofs implemented purely by Lambda Calculus

Question

I've seen often stated that Lambda Calculus can be used for mathematical proofing but I haven't yet seen any example how it is actually used for the task.

Is there a simple example, lambda abstraction or application that can be shown to be a valid mathematical proof? For example what does it take to make a Church numeral successor function regarded as a mathematical proof?