Proving the consistency of Logic in Lean - Viana, Luiz Carlos Rumbelperger (Anais do Workshop Brasileiro de Lógica (WBL); 2020: Anais do I Workshop Brasileiro de LógicaDO - 10.5753/wbl.2020.11452, 2020)
We implement classical first-order logic with equality in the Lean Interactive Theorem Prover (ITP), and prove its soundness relative to the usual semantics. As a corollary, we prove the consistency of the calculus.