桜花爛漫。しかし花見はしていない。
4/8
0時就寝、9時起床。
新しい数学書の情報を入手。フェルマーの最終定理を始めとする大定理たちは数論幾何学を用いて証明された。この数論幾何学、途轍もなく難しいという噂ばかり聞く。そんな数論幾何学の初学者向けの本らしい。気になる～。
arXivを漁っていたら(元)指導教員の名前を見かけた。
Misskey.ioにアカウントを作ってから1周年を迎えた。Twitterの動向が怪しい時期にMisskeyに移住する人が多くいたので、ぼくもみんなについていくように移住した。ぼくのTwitterのフォロワーはほとんどMisskeyには定住しなかったけど、新しい人たちと出会えてよかった。
柏宮花鶏と学ぶ漢字その3を公開した。
Skebリクエストを送って承認された。現在3件が完成待ち。お金が尽きるのでしばらくは依頼しない。
4/9
0時就寝、9時起床。
Skebで依頼していたイラストが早速納品された。とてもかわいい。
組合せゲーム理論を解説する春日部つむぎの動画を見た。今後が楽しみ。ぼくも昔は組合せ論を解説するずんだもんの動画を作っていたけど、チャンネルごと消してしまった。また動画制作に挑戦してもいいかなという気持ちになってきた。
4/10
0時就寝、9時起床。
四字熟語を20個覚えた。
Skebで依頼していたイラストがまた納品された。嬉しい。
タスクをこなした。
久々にポストロック系の音楽を聴いていいな～という気持ちになった。最近は新しい曲を発掘しようとしていない。
女性声優界隈が燻っている。昔は声優ラジオもよく見てたけど、今はもう見ていない。ブルーアーカイブの生放送も見たことがない。
4/11
ブルアカのイベントストーリーをようやく見た。翻訳が微妙という噂を見ていたので読まないつもりだったけど、修正されたので読んだ。
0時就寝、9時起床。
ブラウワーの不動点定理やジョルダン曲線定理について調べていた。
ブルアカのメインストーリーを読んだ。面白いね。世間を騒がせていたハイランダーの双子の名前も判明。
4/12
0時就寝、9時起床。
数学をした。
いろいろな音楽を聴いた。
4/13
0時就寝、9時起床。
漢検1級の模試を解いた。細かいミスで大量に失点して悲しい。
YouTubeでブルアカのメインストーリーの実況を見た。自分だけでは気づかないことがいっぱい。
F*というプログラミング言語があることを知った。proof-orientedというらしい。そういえばLeanも使いこなせるようになりたいなと思っていたのであった。数学とプログラミングの合わせ技という感じがして気になる。
というわけでLeanの勉強を再開した。当面の目標は雪江代数の命題をLeanで実装していくことにしてみようかな。できるかわからないけど。
4/14
0時就寝、10時起床。
癒し系の音楽も好きだけど暗くて陰鬱な音楽も好き。好きな暗い音楽をまとめてみた。Doomer Musicというやつも聴いてみようかな。
またブルアカの実況を見た。
Leanをした。部分群をどう扱えばいいのかまだよくわかっていない。
