近況は標準様相論理の完全性定理をLean4で形式化しており、無事に命題論理の段階で失敗している
様々な目的に使える、日本の汎用マストドンサーバーです。安定した利用環境と、多数の独自機能を提供しています。