docker のトラブルシュートを chatgpt に聞いたらめちゃくちゃ早く解決出来た。こう言うのは LLM 向いてるなぁ
sinon の API とか shell の syntax とか人間が覚えるのがキツい系 API を LLM に聞くのはめちゃくちゃ有効そう
へー、CASIO ちょっと良い機械式時計始めるのか https://www.webchronos.net/news/140163/
このポスト、結構うまく今の AI の特性を言語化できた気がする。
はちゃめちゃなコーディングスタイルで大量にコード書いてライブラリ公開までしてる人がいた。ほとんど AI で書いてたりするのかな
自分が書いてるコードで今の AI で代替出来るものはほとんどないんだけど、ありきたりな Web サービスを作ってる会社なんかだと逆にほとんど AI で賄える感じになってるのかもしれない
こういう別言語の何かを持って来たい系のテクニックは結局何にもならない
https://speakerdeck.com/susisu/tskaigi-2025
頑張るなら TC39 で頑張るしかない。言語に入らないなら流行らない。
CoffeeScript に始まり、あらゆる AltJS が別言語のフリをするのはうまくいかないと教えてくれてる。
ある言語が気に入らないなら、気にいる言語を使うか作るかした方が良い。
そもそも日田じゅんきが黒幕である証拠は無いということは自覚してるのか。見えない脅迫なので、証拠はない、という事をはっきり言っていた。
dagger.io ドキュメント読んでもなんのためにあるのか全然分からなかった。CI/CD のための独自ランタイムがなんで必要なのか分からない。Docker のクリエイターの Solomon Hykes がやってるらしい
日田じゅんきを疑っている理由がなんとなく分かった
NORQAIN 欲しい時計ないなぁ・・・
ライアンと適当に雑談してたら、ライアンはシンギュラリティ起こる派だという事が分かった、自分は起こらない派なので、色々と意見が聞けて面白かった
与沢劇場、色々と気づいたのか、ほぼ全部のデータが消されていて (Youtube は通報から消されたという説をみんな言ってるけど) なんだか平和になってた
与沢劇場本当に怖くなってきた。ここまで具体的におかしくなっていく様がライブ配信されているのは気持ち悪すぎる
差別主義者というレッテルで差別してて草 https://bsky.app/profile/matope.bsky.social/post/3lo6wgejw3227
AI にプログラミングさせるのって、得意じゃない子に無理やり得意じゃない科目やらせてる感じがする
AI が得意なのはどちらかという、コミュニケーションだけの仕事、常識があればあるほど良い、でも専門知識はそれほどいらない、細かいことで間違えてもそこまで問題にならないタイプの仕事だと思う
英語での言い方がわからない場合は、もう deepL で聞くより chatgpt で聞いた方が何倍も良い答えが返ってくる感じがする
deepL はあり得そうな翻訳候補を何件か出してくるだけ (しかも、あまり変わり映えのしないバリエーションしか出してこない)。chatgpt は表現の固さの違うバリエーションとか、いろんなパラメータを変えながら翻訳したパターンを出してきて、自分の欲しい表現にとても辿り着きやすい。
LLM って論理的思考みたいなハードスキルはダメだけど、挨拶とかソフトスキル的な面はとても良くできてる
なんだか人間よりも人間ぽくて、自分の方が LLM よりも機械っぽい
2 + 2 = 4 の証明、ナイーブにプロトタイピングしたら、なんだかとても滑稽な感じになってしまった・・・、
theorem 2 + 2 = 4 {
4 = S(3)
3 = S(2)
4 = S(S(2))
2 = S(1)
4 = S(S(S(1)))
1 = S(0)
4 = S(S(S(S(0))))
2 + 2 = 2 + S(1)
2 + 2 = S(2 + 1)
2 + 1 = 2 + S(0)
2 + 1 = S(2 + 0)
2 + 0 = 2
2 + 2 = S(S(2 + 0))
2 + 2 = S(S(2))
2 + 2 = S(S(S(1)))
2 + 2 = S(S(S(S(0))))
2 + 2 = 4
QED
}
広末とか与沢翼とか、それまで成功していたのに40代で急に自滅してしまう人の気持ちがなんとなくわかる気がする。体が悪くなって、調子が出なくなって、こんなはずじゃないっていう焦りから負のスパイラルに入っちゃうんだろう
lk-proto での最初の課題、フェルマーの小定理とか難しい事言わないで、2 + 2 = 4 ぐらいに設定した方が良さそうだ
AI って論理的思考みたいなところは全然ダメだけど、お笑いのセンスみたいなところはめちゃくちゃ鋭い気がする。
あくまで自然言語から学習しているから、そういうコミュニケーション的な部分の方がだいぶ発達してるのかもしれない
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つ必要な推論規則の扱いが難しい・・・、これがあることで証明がすごくごちゃごちゃした感じになってしまうし、読みづらくなってしまう・・・
プログラミングだと、こういう状況あまり無い気がするなぁ・・・