This is a formalisation of the proofs for the soundness & completeness theorems of classical propositional logic with the ⋀, ⋁, ⊥, ~ connectives in Lean, submitted as my first project for Imperial's Formalising Mathematics module.
alyata/formalising-math-1
Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|
