In this paper we present a formalization of Intuitionistic Propositional Logic in the Lean proof assistant. Our approach focuses on verifying two completeness proofs for the studied logical system, as well as exploring the relation between the two analyzed semantical paradigms - Kripke and algebraic. In addition, we prove a large number of theorems and derived deduction rules.

翻译：本文介绍了在Lean证明助手中对直觉主义命题逻辑的形式化。我们的方法侧重于验证所研究逻辑系统的两个完备性证明，并探讨两种分析语义范式——克里普克语义与代数语义——之间的关系。此外，我们证明了大量定理并推导了相应的演绎规则。