Formalized Formal Logic

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

Notable Results

To find more results, refer Catalogue, Zoo and README of repositories.

• Propositional Logic
  • Classical, intuitionistic and intermediate logics.
  • Kripke semantics and completeness for logics.
• First-Order Logic
  • Completeness theorem.
  • Cut-Elimination theorem.
  • Gödel-Gentzen translation.
• Arithmetic
  • Gödel’s 1st and 2nd Incompleteness Theorem.
• Set Theory
  • Consistency of ZFC.
• Modal Logic
  • Kripke semantics and neighborhood semantics, completeness w.r.t. the semantics.
  • Modal companions.
• Provability Logic
  • Solovay’s arithmetical completeness theorem.
• Interpretability Logic
  • Veltman semantics and soundness for logics.
• Linear Logic

Repositories

• Foundation: Main repository of our results.
• Catalogue: Detailed description about our results.
• Zoo: Diagrams of strength of logics.

Publications

No publications in now.

Talks & Presentations

1. 野口 真柊 『標準的な様相論理のLeanでの形式化について』(in Japanese), TPP 2024: 20st Theorem Proving and Provers Meeting, Dec 2024, Kyushu University. Slides (PDF)
2. 齋藤 彰悟 『Leanを用いたGödelの第一・第二不完全性定理の形式化』(in Japanese), TPP 2024: 20st Theorem Proving and Provers Meeting, Dec 2024, Kyushu University. Slides (PDF)
3. 野口 真柊 『解釈可能性論理の形式化についての報告』 (in Japanese), TPP 2025: 21st Theorem Proving and Provers Meeting, Dec 2025, Tohoku University. Slides (PDF)
4. 齋藤 彰悟 『Leanによる集合論の形式化』(in Japanese), TPP 2025: 21st Theorem Proving and Provers Meeting, Dec 2025, Tohoku University.

Developers

• Palalansoukî (Shogo Saito / 齋藤 彰悟)
  • GitHub: @iehality
  • e-mail: palalansouki@gmail.com
• SnO2WMaN (Mashu Noguchi / 野口 真柊)
  • GitHub: @SnO2WMaN
  • e-mail: me@sno2wman.net

Contributing

We welcome all kinds of contributions, questions, and discussions related to the formalization of mathematical logic.

How to Contact / Proposing Idea

Please open a new topic at GitHub Discussions.

The reason is simple: handling similar inquiries individually (for example, requests for advice on formalizing a particular area) can easily lead to duplicated effort.

If you do not have a GitHub account or you think your message should remain confidential, please send an email us using the contact information provided on the developers section.

Language

We primary use Japanese in discussion, but English is also ok.

Financial Supports

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

Open Collective

We would like to thanks the following backers.

Previous Backers

Individuals and organizations that have supported us in the past.

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

This site is open source. Improve this page.