Switch 2 当選!

初めて実戦で smothered mate (窒息詰み) で勝った https://www.chess.com/live/game/137725093498

React に対する風向きが相当ネガティブになってきてる

これだけユーザーの話を聞かないで、やりたい放題やっていたら然もありなんという感想

主なメンテナーがみんな Vercel に行ってしまったあたりから完全に方向性がおかしくなっている気がする

最近の React がやってる事って基本的に RSC の押し付けでしかなくて、ほとんどのユーザーはそんなもの欲してないしむしろ拒否してる

もう誰も今の React が良いと思ってない

React チーム以外誰も良いと思っていないのだけど、恐ろしいのが React チーム自体がここ最近ユーザーの話を聞く能力が圧倒的に無くなっているので、おそらく今後も方向性が変わることはない。むしろ React チームは今の方向性が最高と思ってそうな節がある。

Angular 2 の頃の Angular チームと Angular コミュニティのズレと同じくらいの根本的なズレがある

Gentzen の LK にインスパイアされた proof verifier のプロトタイププロジェクトを始めた。とりあえず tokenize まで

https://github.com/kt3k/lk-proto/blob/5c18876c689c23d9e8089f945c3b388306d64e33/main.ts

世の中 AI の話だらけになってきてる・・・

Vibe コーディング、まともな技術トピック的に語られてるの草

MCP 出てきてやっと AI に興味持てた。

AI は基本的にちゃんとした知性みたいなものは持ってなくて、馬鹿でかい記憶力と、それなりの判断力がある変なやつという感じで、MCP で AI に対する入力部分がプログラマブルになったことで、効率的に AI に入力を与えられるようになった。

つまり、AI の得意な部分をうまく活用する方法が出来た。

オランダに Lekkerkerker って苗字があるらしい。なんかおもろい https://en.m.wikipedia.org/wiki/Lekkerkerker

wikipedia の sequent calculus のページを一生読んでる (そして一生読み終わらない)

Next 相変わらず誰も求めてない機能ばかり作ってる https://github.com/vercel/next.js/pull/77992

どうしてこんなにユーザーの声を聞かないプロジェクトになってしまったんだろう

巷の教科書の証明と、証明論の定義する証明のギャップは何かなと考えた時に、巷の証明は不明瞭に大量の推論規則を持っているという点がありそう。

「xxの定理より」みたいな推論ステップをよく見かけるけど、これはその定理を適用することを推論規則化して使っている。形式的論理体系ではこういう推論規則は普通は定義しない。

証明論の本て、証明とは何かを定義しているように見えるけど、実際のところ、巷の数学書を眺めると、証明論の本が定義するような仕方で定理を証明している本なんて何処にもない。

定理の適用、推論規則の適用に関して、数学書の証明はとんでもない量の飛躍をしている。

τὰ τῷ αὐτῷ ἴσα καὶ ἀλλήλοις ἐστὶν ἴσα.

Things which are equal to the same thing are also equal to one another. (a = c & b = c -> a = b)

Euclid's Elements, Common Notion 1

σημεῖόν ἐστιν, οὗ μέρος οὐθέν.

入力となる式が2つ必要な推論規則の扱いが難しい・・・、これがあることで証明がすごくごちゃごちゃした感じになってしまうし、読みづらくなってしまう・・・

プログラミングだと、こういう状況あまり無い気がするなぁ・・・