Formalize formal logic (mathematical logic) in Lean Theorem Prover.

Our main repository is Foundation. See Book (In progress) and Doc for more results and details.

• Propositional Logic
  • Completeness for Classical Logic
  • Kripke Semantics for Intuitionistic Logics and Superintuitionistic Logics.
• Intuitionistic and Classical First-Order Logic
  • Arithmetic and Set Theory
  • Completeness Theorem
  • Cut-elimination of First-Order Sequent Calculus (Gentzen's Hauptsatz)
  • Gödel's First and Second Incompleteness Theorems
  • Solovay's Arithmetical Completeness Theorem
• Basic Modal Logic (with modal operators $\Box, \Diamond$)
  • Kripke Semantics and Completeness
  • Modal Cube
  • Modal Companion
  • Provability Logic
• Interpretability Logic

• Palalansoukî (Shogo Saito, @iehality, ✉️:palalansouki@gmail.com)
  • Overall design and maintenance.
  • First-order logic.
  • Intuitionistic first-order logic.
  • Proof automation.
  • Provability logic.
• SnO2WMaN (Mashu Noguchi, @SnO2WMaN, ✉️:me@sno2wman.net)
  • Modal logic.
  • Propositional logic (including intermediate logic).
  • Provability logic.
  • Interpretability Logic.
  • Miscellaneous repository maintenance (e.g. GitHub Actions)

Any financial supports would be grateful for us. If you found this project valuable, to sustain our OSS development, please consider support us.

We would like to thanks the following backers.

Individuals and organizations that have supported us in the past.

• Proxima Technology (2024-2025)
• 随時 (@zuizi) (2025-10)