2025 年の抱負です。

今年の M1 のファイナリストじゃないひとたちで、おもしろかった人を褒めます。

aesop タクティクで手軽に自動証明をします

なぜ私は落ち込んだ時に（落ち込んでないときにも）散歩に行くのか

アイデア記事

私のプログラミング遍歴

そういうこともあります

2024年買ってよかったもの

【有料記事】昔親友だった人の話

【有料記事】日記です。

Lean 関連活動振り返り

【有料記事】日記です

TPP2024の2日目の感想

TPP 2024 に聴講参加したので、その１日目の感想を書きます。

【有料記事】私の人生の話です。

zenn に投稿を始めました

【有料記事】愚痴です

11月になったので振り返り

foldlM が必要になるケースです。

繰り返し自乗法は Lean のライブラリに既に存在するのか？

日報というタイトルにしましたが、毎日やるとは限らなくて、不定期に投稿していくつもりです。 繰り返し自乗法 今日は Lean で繰り返し自乗法の実装をしました。これは、x ^ n の計算を行うためのアルゴリズムです。 普通の、多くの人が考える素朴なアルゴリ…

Lean のバイトを新たに発見しました

大学の学部生だったころ、宮崎修一という先生の授業を受けたが、あれは私が計算機科学をおもしろいと思うきっかけだったと思う。あの先生は本当に授業が上手だった。 聴衆にどんどん参加させるタイプの授業だった。定期的にスライドを止めて「これはどうなる…

指導教官がどれだけ教育に熱心かというファクタの重要性について

ビスコを買いました。

Twitter （今ではXと名乗っているアプリ）はやめどきがわからないので、最初から iPhone からでは閲覧できないようにしようと思って、それを実現するアプリを探した。 結論から言うと、良いアプリはなかった。どれも課金を迫ってくるだけのクソアプリで、ど…

自分は頭が悪いなあと思う。 試験に通ったのは頭が良いからではない これを知人に言うと、「京大に入るくらいだから頭は良いはずだ」と返される。でもそれは私の実感とは違う。 大学に入れたのは運と、高校の３年間他のことを捨てて執拗に繰り返し繰り返し勉…

いままであまり書いていなかったような気がするのですが、「個人ではなくコミュニティが成長する」というのは Lean の大きなメリットだなと思います。 どういうことかというと、「人間が手動で証明を検証する」いわゆる普通の数学と、Lean などの定理証明支…

数学をやり直したい

これは私ではなくて知人の話なんですけど、某 n もん式塾で算数を習っているときに、「どうして１は一つしかないのか」「どうして１に１を足すと２になるのか」というのが疑問だったそうなんですね。 それで先生に質問したら、「そう決まってるから」という…