Lean4 formalizations of famous model-theoretic and proof-theoretic theorems

As of writing this, I have written soudness and completeness proofs in Lean for the normal modal logics K and S5. I am currently working on implementing similar proofs for quantified modal logics.