The Church–Rosser theorem is a central metamathematical result about the lambda calculus. This chapter presents a formalization and proof of the Church–Rosser theorem that was verified using the Boyer–Moore theorem prover. The proof presented in this chapter is based on that of Tait and Martin-Löf. The mechanical proof illustrates the effective use of the Boyer–Moore theörem prover in proof-checking difficult metamathematical proofs. The syntactic representation of terms turns out to be crucial to the mechanical verification. The form of the formalization often significantly influences the ease or difficulty of a verification. We also compare the length of the proof input to the Boyer–Moore prover with the lengths of various informal presentations of proofs of the Church–Rosser theorem.

The lambda calculus was introduced by Church [Bar78a, Chu41] in order to study functions as rules of computation rather than as graphs of argument–value pairs. It was hoped that the lambda calculus would provide an alternative foundation for logic and mathematics. This aim has remained unfulfilled due to the appearance of contradictions when the lambda calculus was extended with logical notions. The lambda calculus has nevertheless been a fruitful medium for the study of functions and computations. The programming language in which the mechanical proof was formalized, a variant of pure Lisp [MAE+65], was one of the first languages whose design was influenced by the lambda calculus.