近況としては主に戸次『数理論理学』に基づいて(最小/直観主義/古典)命題論理をLean4で形式化しているが、まだ殆ど何も示していない（せいぜいHilbert流体系について整理したのみ）

https://github.com/SnO2WMaN/lean4-propositional-logic