初めて実戦で 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つ必要な推論規則の扱いが難しい・・・、これがあることで証明がすごくごちゃごちゃした感じになってしまうし、読みづらくなってしまう・・・
プログラミングだと、こういう状況あまり無い気がするなぁ・・・
UX の良い proof verifier を作ろうと思うと、推論規則を結構沢山用意しないとなかなか使い物にならないかも
かと言ってあまりにも多くの推論規則があると「覚えられない」となりそうなので、なかなか難しい・・・
a0. some a { all b { S b != a } }
d0. let 0 { all a { S a != 0 } }
a1. all a b { a = b -> b = a }
a2. all a b c { a = b & b = c -> a = c }
a3. all a b { a = b & b is Nat -> a is Nat }
a4. all a { a is Nat -> S a is Nat }
a5. all a b { S a = S b -> a = b }
a6. all a { S a != 0 }
a7. all pred K { K 0 & all a { K a -> K S a } -> all a { K a } }バビロン捕囚のバビロンと、キュロスが征服したバビロンが同じものだと分かって、聖書世界と古代ギリシャ世界がグッと近いものに感じられるようになった
みんな AI 好きだなぁ・・・
完全系列 (exact sequence) という言葉を久しぶりに聞いた。やはり数学書は良いものだ
10進数をちゃんと定義して使う、自然言語も極力制限して使う、みたいな数学書を書いたら面白そう
基本の syntax ぐらいは、練りに練ってからもう breaking change しないぐらいの感じでスタートしてほしいもんだなぁと思ったり・・・
Deno も結構そういうところあるけど、Lean のチュートリアル、ちょっと古いやつだと最新の Lean で動かなくなってるぽいのがあるっぽくて注意が必要そうだ・・・
lean4 関数適用式で括弧省略するタイプか・・・嫌いだなぁ
数学者、10進数を定義しないで使いがち
bijective base n もそうだけど、times が全般的に JSR 移行されていないので、そろそろしておこう・・・
bijective base n まだ JSR に移して無かった・・・、今度移行しよう・・・、このライブラリここ数年で自分が書いたモジュールの中で一番好きかも・・・
Lean 4 公式の install 方法が VSCode 経由なのか https://lean-lang.org/lean4/doc/quickstart.html
test
UUID って 6 bits (4.7%, ver + var) をシステムと関係ないメタ情報で使わされてるし、使う意味ないんじゃないかなぁ・・・エンコーディングが非効率的な hex なのも何だか意味がわからない
UUIDv1 = time_low + time_mid + ver + time_high + var + clock_seq + node
UUIDv6 = time_high + time_mid + ver + time_low + var + clock_seq + node
最初の総理大臣就任が明治18年なの面白いなぁ。それまでの国の代表は誰なんだろう?
なんとなく Paul Valéry の La Jeune Parque という作品に興味を持った。フランス語やってて良かった
Parque というのはファイブスター物語でお馴染みの運命の3女神 (ラケシス、クローソー、アトロポス) の事らしい