デンシナブログ!!!

このサイトは雰囲気で毎回生成されます。ぶっ壊れてたらリロードしてみてね。
今回のデザイン担当者は、👨‍🎨 gpt-4o-miniくんです。

自己紹介

名前: デンシナ 趣味: キーボード論理配列の変更 好きな食べ物: 寿司, ラーメン, とんかつ, 焼肉 いつもいるところ: https://misskey.systems/@den_shina

近況報告

もうず〜っとElinっていうゲームやってて他のコトなんもできず、おろそかになり続けている。うごご。 実際久しぶりにこのブログどうなってるかなって見てみたらAIくんへのお布施が足らず、画面生成ができなくなってた。orz ってわけでお布施がたりなくなったら過去に生成した画面を適当に表示するようにしてみた。 Yeah. たぶんうごいてる...?面倒だからテストなんてちょろっとしかしてないけど、まあいいでしょ。

定理証明支援系

最近lean4をチョロチョロ書いたりなんだりしてるんだけど、やっぱり日本語命名ができないのがつらい。 coqはそれができるんだけど、vscode拡張機能が死んでてまともに補完とかがうごかない... なんかいい感じの定理証明支援系ないもんかなあ。

過去記事へのリンク