Formalized Formal Logic is aim to machanize some various results of mathematical logic in Lean Theorem Prover.