Someone else gave a very good definition, but I'll add that historically, the Lambda Calculus was a system designed by Alonzo Church to get a formal notion of w

Someone else gave a very good definition, but I'll add that historically, the Lambda Calculus was a system designed by Alonzo Church to get a formal notion of what "computation" means in mathematics. As in, a formally-defined set of rules for how a computation can be represented, and then be mechanically carried out to achieve a result. The need for such a system came about because of mathematicians wanting to define what it means for a function to be computable in a formal sense, and to be able to define and prove other theorems about computation. The other famous model of computation, which was invented at about the same time, was Alan Turing's "Turing machine", which he used to prove that the halting problem was not computable. Just for a short taste, in the lambda calculus the base entity is an abstract function that can be applied to a variable and return a result. You are probably familiar with formulae like `f(x) = x`. In the lambda calculus formalism, this is written as `\lambda x.x`. However, it's important to note that there is no direct equivalent to something like `f(x) = x + 1` - addition or numbers are not a part of the lambda calculus directly. Instead, you can define numbers and then addition in terms of functions and variables. Instead, the lambda calculus has rules for how function application should work to reduce complex formulae to simpler ones. For example, `(\lambda x.x) y` reduces to `y` [equivalent to f(x) = x; f(y) = ? => y]. Or, `(\lambda x.y) z` reduces to `y` [equivalent to f(x) = y; f(z) = ? => y]. And, if we go on to more complex expressions: `(\lambda x.x) (\lambda x.y) z` reduces to y by applying the reductions above successively (first we reduce the initial expression to `(\lambda x.x) y` then we reduce this to just `y`. It can be shown that this model of how to reduce the formulae of lambda calculus is in fact equivalent to the model of the Turing machine that can write a symbol on its tape.