  This paper presents a recent formalization of a Henkin-style completeness
proof for the propositional modal logic S5 using the Lean theorem prover. The
proof formalized is close to that of Hughes and Cresswell, but the system,
based on a different choice of axioms, is better described as a Mendelson
system augmented with axiom schemes for K, T, S4, and B, and the necessitation
rule as a rule of inference. The language has the false and implication as the
only primitive logical connectives and necessity as the only primitive modal
operator. The full source code is available online at
https://github.com/bbentzen/mpl/ and has been typechecked with Lean 3.4.2.
