2024.12.03
https://gyazo.com/1736fc70e0c904479456bbf712e83623
DJをするときの名義のアイコンーを描いた
前：
2024.12.02
後：
2024.12.04
#日報
お知らせ
証明支援系AdC2024
の3日目の記事を書きました．
ちょっと前に，論理パズルで有名なスマリヤンが一般向けに不完全性定理などを説明するために導入した非常にシンプルな形式体系をLeanで形式化したのですが，その解説記事です．Leanの形式化自体は300行程度しかなく素朴なので，ここにいる人ならコード全部読んでみるとおもしろいかもしれません．
https://github.com/SnO2WMaN/notes-on-smullyanTP
notes-on-smullyanTP
#証明支援系アドベントカレンダー2024