Proving confluence and strong normalization for lambda calculi is fundamental to programming language semantics, but no comprehensive, modular framework for these proofs existed in Lean 4.

The authors present Metatheory, a library for programming language foundations in Lean 4 featuring a modular framework for proving confluence of abstract rewriting systems using three classical techniques: the diamond property, Newman's lemma, and the Hindley-Rosen lemma. These are instantiated across six case studies including untyped lambda calculus, combinatory logic, term rewriting, simply typed lambda calculus, and STLC with products and sums. The library includes complete proofs of de Bruijn substitution infrastructure and demonstrates strong normalization via logical relations.

All theorems are fully mechanized with zero axioms or sorry statements. The framework covers six case studies and provides the first comprehensive confluence and normalization framework for Lean 4.