サブタイトルつけるの飽きました。
5/6
0時就寝、6時起床。疲れているときは睡眠が下手。
サイクルを禁止したときのTurán numberについて学んだ。
新しい動画を作り始めた。
yukicoderで作問してテスターを募集した。
GW最終日ということで、GWにちなんで勉強していたGW不変量の勉強記録を公開した。
いやあ、もっとやる気があればちゃんとGW不変量を理解できたかもしれないけど、怠惰だった。GW不変量って、なんなんだ。当面はGW不変量の勉強は休止して、大好きな組合せ論に戻ろう。
5/7
0時就寝、7時起床。
Leanで組合せ論の定理を実装する話を見た。ぼくもLeanで定理を実装したい。
というわけでLeanを触った。せっかくならmathlibに頼らず群論を実装してみようと思った。いまいちよくわからない。難しいねえ。
Dependent random choiceという手法を知った。
5/8
0時就寝、5時起床、7時再就寝、10時再起床。起きている間は数学をしたり作問した問題について考えていた。
学マスの楽曲が公開されている。とりあえず一番気になっている篠澤広さんの曲を聴いた。いいですね。他の曲も聴かなきゃ。
動画が完成したけど、出来が微妙。作り直そうかな。
競プロの作問をしていた。
5/9
0時就寝、8時起床。
今まではTurán numberの上界を考えていたけど、下界を考えるパートに突入。いろいろな方法でグラフを構成する。
昨日まで作っていた動画を没にして、新しい動画を作り始めた。
数学の動画を見た。log-concave多項式の話は2年前くらいに記事にするために調べた。なんか不等式を紹介していた。巡回セールスマン問題に応用されていたのは不思議な繋がりで面白い。もっと調べてみたい。
5/10
0時就寝、8時起床。寝る前と寝起きの数学タイムが毎日の楽しみになってきている。
PCで見るTwitterの表示が少し前からおかしいなと思っていたけど、GoodTwitter2をオフにしたら直った。でもこのTwitterのUIは慣れない。どうしよう。その後フォントのせいという情報を得て、直すことができた。Stylusでspacingを調整した。GoodTwitter2のままでTwitterができる喜び。
動画が完成したので投稿した。基礎から解説しているけど、はやく深淵まで行きたいね。
June Huhへのインタビュー動画を見た。数学の内容ではなく、数学を志す人へのメッセージといった感じだった。
yukicoder contest 429に1問出題した。またこの人カタラン数に関する問題出してるよ。大昔にテスターをした問題も出題されていた。競プロを長らくやっていないのでテスター応募も控えていたけど、やっていきたい。そのためにも競プロ力を取り戻さないといけない。
5/11
0時就寝、8時起床。
動画を作った。
家族と買い物に行った。
ABCに参加した。Aははい。Bはざっと読んで実装する。Cはちょっと難しい。108を引くかそのままかの2通りで、和が108以上になるのがいくつかを判定する。ソートして二分探索を使った。Dは分ければよい。Eは未履修っぽい。Fはめんどくさそう。Golfを思い出した。前回は好成績だったけど、今回は微妙。
5/12
0時就寝、8時起床。
Graph Theory and Additive Combinatoricsの一章をざっと読んだ。部分グラフの禁止がテーマで、確率論や代数幾何などの様々なテクニックが使われている。面白かった。
Leanで群論の定理を実装するプロジェクトを進めた。雪江代数1をまるごとカバーできたらいいなと思っている。それができたらある程度Leanには慣れているはずだし、もっと高度な定理を実装してみたい。
YouTubeに動画を投稿した。Mantelの定理に続いて、Turánの定理も証明した。いろいろな証明があると動画内でも触れているけど、Graph Theory and Additive Combinatoricsには5つある。この本に載っている他の定理も解説したい。
