SnO₂WMaN @sno2wman@fedibird.com

名は体を表すので名字をFalsemannにしたい

第一線の人でもSahlqvist論理式のSahlqvistの読み方が何なのかははっきりしていないらしくてそんな…と思った

近況:　「容易に示せる」→　容易に示せるのか〜　→　シッチャカメッチャカに…

日報(2023.07.10)

https://scrapbox.io/sno2wman/2023.07.10

日報(2023.07.09)

https://scrapbox.io/sno2wman/2023.07.09

#日報メモ　調べてないからわからないが国会図書館って本の帯はともかくとしてカバーも廃棄して記録してないのか？

日報(2023.07.08)

https://scrapbox.io/sno2wman/2023.07.08

日報(2023.07.07)

https://scrapbox.io/sno2wman/2023.07.07

日報(2023.07.06)

https://scrapbox.io/sno2wman/2023.07.06

ドキュメントを流し読みしているのが一番悪いとはいえMathlib4の証明を読んで「こんなtacticsあるんだ」みたいな発見をすることが多々あり、さておきLean4のドキュメントは利用例も含めて少なすぎるので、日本語圏での普及を目的として何かしらのWikiとかを作って啓蒙/連帯したすぎる

長らく1100回ぐらい手動で行っていた日報のツイートはここでは自動で投稿するようにしたい

皆がこの問題にどのように対応しているのか不明すぎる

近況は標準様相論理の完全性定理をLean4で形式化しており、無事に命題論理の段階で失敗している

ここは静かで、寂しい