A lambda encoding is some way of representing data as functions (lambda abstractions).\xa0 Some motivations for this for computer-checked proofs and type theory.