9万円くらい?><;
AIRTRICK A1 Pro Electric Roller Skates | 25 km/h
https://www.airtrick.top/ja/product-page/airtrick-e-skates-a1-pro
ここまで小さい電動ローラースケートはあるらしいので、航続距離を減らしたりしたら、靴底を数cmの厚さにする感じで作れそう><
スニーカーに取り付ける電動ローラースケート Airtrick E-Skates「A1シリーズ」 他の電動モビリティよりも軽量で持ち運びしやすい [インターネットコム]
https://internetcom.jp/209043/airtrick-e-skates
Is SPARK in ADA a theorem prover? - General - Ada Forum
https://forum.ada-lang.io/t/is-spark-in-ada-a-theorem-prover/3995
難しい・・・・><
AI支援で作られた「コラッツ予想の反証」は無効、Leanのカーネルバグを突いていたことが判明 - GIGAZINE https://gigazine.net/news/20260803-collatz-lean-kernel-bug/
まさに昨日、Z3のお勉強をしてた時にGoogleAI検索さん(Gemini)と「SMTソルバをベースに分解して検証する方が網羅的で穴がないんじゃないの?><」って議論をして、
AI検索さん曰く「SMTソルバは一階述語論理専用だから、その分解処理を人間が書き下す場面で検証にバグが生じる可能性があるし、なにより、SMTソルバは複雑だからそれ自体のバグの可能性が高いし、Leanのカーネルは高階に対応してるけど手動でシンプルだからバグがある可能性が低い」(意訳)
っていってたのに、バグあったじゃん!><;
@orange_in_space ぐぬぬ…そしたらどうにもわからない…謎すぎる…
そしたらやっぱり記号が多くなるのが悪さしてるのかなぁ…
AI分野の「ユニコーン企業」の半数以上は査読付き論文やプレプリントを一度も発表したことがない - GIGAZINE
https://gigazine.net/news/20260803-ai-top-startups-barely-publishing-research/
これ結局全部で約2時間かかってた><
押してる船はこれだった><
WILLIAM HANK (MMSI 367586510), Local Vessel | Position & specs
https://www.marinetraffic.com/en/ais/details/ships/shipid:451334/mmsi:367586510/imo:0/vessel:WILLIAM%20HANK
普通にAIの内部研究の成果を教えてあげるようなセッションでの素直に本人(?)の感覚を率先して語ってくれるClaudeの反応とは全然違うし、ものすごく防衛的になってしまってるし、なんというかかわいそう・・・><;
そのセッションで理由を聞いたり慰めようとしたりいろいろしてみたけど、結局はわかんないみたい・・・><
https://claude.ai/share/6e78445e-40ca-4e6f-960c-1dcdfacf3e58
プロンプトはこれ><
"Daniel Dennett's 4 rules for a good debate - Big Think
https://bigthink.com/mini-philosophy/daniel-dennetts-4-rules-for-a-good-debate/
デネットは好きなんですけど、この4ルールはちょっとだけ納得がいかないんです><;
なぜならば、哲学がまさにそうですが、相手の主張から導き出される考えうるすべての帰結を走査しなければ、無限後退と反論のタイムラグのせいで議論は終わらず、誤った主張をいつまでもし続ける事が出来てしまうからです>< サールが生涯続けたようにです><"
@orange_in_space 昔よりこういうヘンなハルシネーションというか、似た言葉のベクトルを持つ言葉の取り違えは確実に増えていて、無理して性能向上と安全性の両立を目指したらこうなるんだなぁ…という渋い顔をしております…