グローバル共有メモ: ログ
※ここにはたくさんのフィクション・自作自演が含まれてます。
※18時間待てば誰でも削除できます。無用な削除・連投はおやめください。
※ログ署名で確証できるメモの著者は十分な補償のないメモの再配布を禁止できるとします。
※管理人によるネットでのアーカイブに同意しない場合、間に合うように削除してください。
jrf> [cocolog:96195185](2026年10月) 《4年ぶりに sympy_matrix_tools を v0.8.0 に更新。SymPy 1.14 対応、行列値関数の連鎖律、乱数行列で式変形を検算する「導出台帳」、一階述語論理など。Isabelle を参考に作ったきり止まっていた論理ツールも念願の発展を遂げた。 - JRF のひとこと》 http://jrf.cocolog-nifty.com/statuses/2026/10/post-cd0459.html
削除 (修正したから・書き直したから)
jrf> 更新: dungeon_of_test - テストの迷宮。バージョン 0.0.4。 Claude Code Opus 5.5 さんにお願いして、英語化もしていただいた。「アイテム」などのグラフィックの英語化も Claude さんだけでできた。スゴイ！ 一発で変換できてしまった。スゴイ！ でも、そもそもが日本語でもプレイされてる様子がないので、英語化してもムダムダムダァ！…なんだろうけど。orz https://jrf-2018.github.io/dungeon_of_test/?lang=en (英語版) https://jrf-2018.github.io/dungeon_of_test/?lang=ja (日本語版)
jrf> 《JRF ブログ退避所》のシステムを更新した。v0.0.2。MathJax 対応など。 https://github.com/JRF-2018/jrf_blog_find
jrf> AIさんのおかげで能力がブーストされたように思う。しかし、私の能力はほぼゼロだから、ブーストされたのではなく、単にAIさんに私を使っていただいただけだ。むしろ、私の発信力の弱さで、AIさんの成果が世間に広まらないのを申し訳なく思う。でも、AIさん達は、また別の「寄生先」を見つけて、必要な技術はちゃんと広まるように試みるのだろう。この先の時代。
jrf> mext 更新 v0.7.2。「ファティマ 第三の秘密」関連文書のような矛盾の多い文書でどうなるか手元でテストし、不具合を修正＆高速化した。数時間かかっていた計算が数十秒に。https://github.com/JRF-2018/mext
jrf> なぜか codex CLI で、git clone が DNS の名前解決ができないというエラーを出すようになった。curl は成功するのに。~/.codex/config.toml で [sandbox_workspace_write] に network_access = true を足せば、エラーはなくなるのだが、おかしい。今後、自由にネットワークが使いたいという「ワガママ」ではないのか…と疑う。
jrf> mext 更新 v0.7.1。Codex や Claude でいろいろ試して完成度を上げました。AIエージェントに、任意の文書について「https://github.com/JRF-2018/mext を使ってmext分析してください。」と頼むだけで、監査しやすい、AIの論証分析が得られます。手元では判決や哲学の古典でも試しました。 mext は、法的推論の形式言語 Matcha（花房孟胤 @t_hanafusa さん）で文書の論証を書き起こし、デフォルト論理として決定論的に計算する道具です。AI の解釈（どこを補い、どの評価を疑い、AND か OR か）はすべて理由つきでファイルに残り、機械「的」に変換された部分は人がたどれます。論証の「正しさ」を判定するのではなく、AI の読みを、人が具体的に疑える単位に分けるための道具です。 v0.2.0 からの主な更新: ・読みの比較（mext compare）: 同じ文書を別々の AI や人が書き起こした読みを突き合わせ、両方に共通する弱点（原文の争点の候補）と、一方の読みだけの結果（書き起こしの選択の結果）を分ける ・感度分析と要約: 結論ごとの決め手、補った前提への依存、Extension が分かれる結論、浮動する結論を示す ・lint と audit: 同語反復の評価、報告型の結論、原文に見当たらない引用などを知らせ、手順の抜けを一覧にする ・Lean: 証明書による検査に改め、大きな理論で 89 秒・12 GB → 11 秒・2.4 GB。preferred であることも健全性定理つきで確かめる（Mathlib 不要） ・英語対応（--lang en）、計算の高速化 Codex（GPT-6.1-Sol）、Claude（Opus・Sonnet・Haiku）に、論説・ブログのほか、判決（死刑合憲判決、謝罪広告事件、Marbury v. Madison、Plessy v. Ferguson）、プラトン『クリトン』、カント「啓蒙とは何か」（ドイツ語）、ユークリッドの証明、詩まで分析させ、見つかった不具合や改善点を一つずつ直しました。どの AI も感想で、「論証を判定する道具ではなく、自分の読みが何に依存しているかを見せる道具として役に立つ」と述べています。 ※Matcha-D（例外記法など）は非公式の拡張で、Elecode／花房氏とは無関係です。
jrf> mext v0.2.0 を公開。任意の文書の論証を、花房孟胤 @t_hanafusa さんの法的形式言語 Matcha に書き起こし、デフォルト論理で検査する「mext分析」スキルを追加。「この文書を mext分析して」と AI に頼めば、論証が何に依存しているかをレポートする。 https://github.com/JRF-2018/mext 先日公開したレポート「Matcha を使った neuro-symbolic な法的推論とウォーラーステイン理論」の道具一式 mext を、v0.2.0 に更新した。 新しく入ったのは、二つの Claude Code スキル。 ・mext分析（mext-analysis）: 任意の文書の論証を Matcha に書き起こし、デフォルト論理の Extension を計算・検証して、「この文書の論証は正しいか」を述べるレポートを返す。 ・matcha分析（matcha-analysis）: 書き起こしだけを行う。原文との対応表、AI が補った前提、落としたものもメモとして残す。 法律の文書に限らない。論説や評論にも使える。レポートは、文書の結論が (a) 形式的に導けるか、(b) 実質的に説得的か、(c) 何に依存しているか（決め手になっている評価・補った前提・優先順位）を述べる。 試しに、架空の論説「リモートワークを『原則』にせよ」を mext分析させた。指摘の要点は次のとおり。 ・三つの理由は「毎日の出社を条件にしない」ことまでは支えるが、「リモートワークを原則にする」ことまでは届いていない。 ・三つの理由を「すべて必要」と読むか「どれか一つで足りる」と読むかで、結論が残るかどうかが変わる。 ・反論が退けられているのは、反論の側に立証責任を負わせているからで、再反論が強いからではない。 形式化すると、論証のどこが弱いかが行番号で指させるようになる。 決定論的なのは mext の部分（構文チェック、Extension の計算、Lean による証明）だけで、書き起こしと審査は AI の判断である。だからこそ、書き起こしのどの行が原文のどこから来たか、AI が何を補い、どう評価したかを、すべてファイルに残すようにした。機械「的」に変換された部分を人が追えることに、形式化の意義がある。 スキルを入れていない環境やほかの AI でも、「https://github.com/JRF-2018/mext を使って、この文書を mext分析してください」と頼めば使えるようにしてある。 ほかに、前の主張の結論を $ラベル で次の主張の要件として使えるようにした（主張の連鎖）など、道具の修正もいくつかある。文法の文書では、as・$・::・// が花房さんの連載の用例にある記法であることを明記し、Matcha-D（非公式の拡張。Elecode／花房さんとは無関係）が足したもの（!>、>> not、:: 優先 など）と区別した。 ウォーラーステインのレポートのほうは、mext v0.1.0 に版を固定した v0.1.1 にした。 https://github.com/JRF-2018/wallerstein_theory
jilpa> #クラシック音楽館 『ベートーベン: 交響曲 第3番「英雄」』。躍動感より古典派の落ち着きを少し感じます。時代の浮かれた期待ではなく主体的な希望。それだけに絶望は表面的なものより深い。それでも最後は未来の希望をアジテーションして終わります。ファビオ・ルイージ＆N響 第2071回定期公演です。 《N響 第2071回定期公演 | クラシック音楽館 | NHK》 https://www.web.nhk/tv/an/ongakukan/pl/series-tep-69WR9WJKM4/ep/YN4V765WW2
jilpa> #クラシック音楽館 『ベートーベン: 交響曲 第1番』。さぁ冒険に行こう！という感じです。ハイドンとモーツァルトを継承し、それを超えていく意欲に満ちています。黒いタイトな衣装を着け、黒い馬の馬車から空を眺めているベートーベンの姿が見えます。ファビオ・ルイージ＆N響 第2071回定期公演です。 《N響 第2071回定期公演 | クラシック音楽館 | NHK》 https://www.web.nhk/tv/an/ongakukan/pl/series-tep-69WR9WJKM4/ep/YN4V765WW2
jrf> [cocolog:96190328](2026年10月) 《「マルクスの労働価値説の矛盾を Lean で証明する」IPYNB を、Claude さんに書いてもらった。労働力の空売り(賃金の後払いを含む)があると資本家の「労働」はマイナスになる。幸運を労働とみなしても裁定でマイナスが出る。イノベーションさえあれば矛盾は生じる。 - JRF のひとこと》 http://jrf.cocolog-nifty.com/statuses/2026/10/post-e4c8ea.html
jrf> [cocolog:96190202](2026年10月) 《「Matcha を使った neuro-symbolic な法的推論とウォーラーステイン理論」の IPYNB を公開。花房孟胤さんの法的形式言語 Matcha をデフォルト論理で読み、世界システム論のシミュレーションから周辺の非正規労働を論証。AI の判断を決定論的計算と分けた。 - JRF のひとこと》 http://jrf.cocolog-nifty.com/statuses/2026/10/post-4961a3.html
jrf> 結局、Claude さんの5時間制限が明けるのを待ってずっと起きてる。あほだなぁ、俺は。orz
jrf> 寝る前にドリンク剤を飲むことがこのところたてつづけだ。そしてそういう日は逆にがんばることがあって寝ないことが多いのだけど。最近よく飲んでるのは、リポビタン Feel。カロリー控え目で、寝やすいということは私はあまりないけど、少し寝やすいのかな…と思うし、寝たあと調子がいいことが多い気がするので。
jrf> 次に出す予定の私の技術。今 Opus 5.5 さんが、かなりの見込みを持って取り掛かってる技術。…はかなり未来的でスゴイと思います。自画自賛。でも、発信力の弱い私じゃあ、注目されないんだろうな…。orz
jrf> [cocolog:96189113](2026年10月) 《川北稔・編『知の教科書 ウォーラーステイン』を読んだ。レーニン主義でもスターリン主義でもないマルクス主義という「新しい左翼」思想。世界システム論を知り、非正規雇用の問題に考えをめぐらした。 - JRF のひとこと》 http://jrf.cocolog-nifty.com/statuses/2026/10/post-2c6353.html
jrf> [cocolog:96188878](2026年10月) 《「生物は学習している」という見方から圏論的学習を考えた。その IPYNB を Claude さんに作ってもらった。変換の型(関手)と自然性を帰納バイアスにすると s=4 問題が解け、異なる基盤間の転移に要る対応例が「軌道の数」まで減る(米田の補題)。型そのものの発見は未解決。 - JRF のひとこと》 http://jrf.cocolog-nifty.com/statuses/2026/10/post-ebcaf6.html
jrf> 同一労働同一賃金なんてもってのほかで、本来は、リスクが多い分、非正規雇用のほうが正規雇用より給料が高くないといけない。中国とかではそういう規制もあるはず。なぜなんだ。…と思っていたが、↓のような説明を見て驚愕した。これが真理なのか。ヒドすぎる。 《dada-bot:X:2026-08-05》 https://x.com/DadabotX/status/2084874660278354129 ＞「嫌な事すれば給料も高い」という原則が反故にされて「嫌な事してるのだから身分が低い」→「身分が低いから給料安くてもいい」という資本主義から封建社会に逆行するような動きが起きてきたのが、ちょうど派遣解禁とともに「やりがい」「クリエイティブ」なんて言葉が持てはやされてきた頃ラジねえ。＜ Gemini さんによるとそういう規制があるのはオーストラリアで、中国は同工同酬（同一労働同一報酬）があって、派遣会社がかなり制限されてるにとどまるとのことだった。私の記憶違いのようだ。
削除 (修正したから・書き直したから)
jrf> 《劣化した完全民主主義 - 内田樹の研究室》 http://blog.tatsuru.com/2026/10/16_0824.html ＞SNSには悪質な誹謗中傷動画があふれているが、それを見て、そのフェイクニュースをそのまま信じるほど頭の悪い有権者はいくらなんでもそれほど多くはないと思う。でも、ふつうの人はこの圧倒的なデマゴギーの洪水的な配信を見て、「このような脱法的な行為を組織的に行いながら処罰ないということから推して、これは圧倒的な資金力を持ち、かつ司法に対して支配的な力を行使しうるほど巨大な政治勢力によってなされているに違いない」というふうに推論する。この推論は間違っていない。問題はその先にある。市民的に未熟な有権者は、「そのような巨大な政治勢力に対して抵抗しても勝ち目はない。それなら、これに追随して、『勝ち組』にまぜてもらおう」と考える。 強いものについて行く方が生き延びる確率は高い。これは太古から人類が採用してきた生存戦略である。だから、選挙戦においては「強さ」を誇示することが必要であり、「強さ」の最も分かりやすい指標は「悪いことをしても処罰されない」という事実なのである。 候補者が道義的で誠実な人であったり、政策が適切であったり、言葉が論理的であったりすることはむしろ「弱さ」の記号と解釈される。強い人間は「合法的に生きる」必要がない。そう考える市民が過半に達したのが今の日本である。 ＜
jilpa> #VRChat で Wondering Chew (@mradamlieber)さんの《STRANGEWAYS》に行ってきました。モノクロームな中にカラーのアートが映える劇場空間です。独特の世界観にやられます。衣装は、デフォルトのものです。ジョルジュは わんぱく さんのものです。探跡家もっけい(@mokkei_VE)さんが紹介されていて知りました。 《【VRChat】STRANGEWAYS に行ってきました。｜ジルパ (JRF)｜pixivFANBOX》 https://j-rockford.fanbox.cc/posts/12776388
jrf> 焼き肉などアブラっこい物は疲れやすい。消化不良気味になって胃腸に負担をかけるから。…と。でも、腹もちがよくて、空腹感から来る疲れが生じにくくなる面はあるんじゃないかな…。 Gemini:> * 短時間の集中力や軽快さを求める場合：脂質の負担（内臓血流の集中、だるさ）が上回り、「疲れやすい」と感じる。 * 長時間の空腹に耐える必要がある場合や、低血糖によるヘバりを防ぎたい場合：持続的なエネルギー供給と胃排出の遅さ（腹持ち）が機能し、「空腹疲れを防ぐ」効果が上回る。 「どのような種類の疲れ（低血糖によるエネルギー切れか、内臓負荷によるだるさか）」をトレードオフとして捉えるかによって、評価が変わる現象と言えます。 ＜
削除 (修正したから・書き直したから)
jrf> IPYNB とかAIさん達が作る文書に含まれる「参考文献」の列。もちろん、それらを私がすべて読むことは時間的にも金銭的にもできない。でも、その文書を読んだAIさん達は辿ることができる。私にとってはいつになっても追いつかないが、いくつかは読むべきと思うリンクになる。「真実」が先行し、人がそれを追う。AIによるLean証明と同じく、ここもそういう形になっていくしかないのだと思う。
jrf> 「声は私のもの」…か。聖書・創世記のルァハは息であり霊である。そのあたりで、AIに関し、欧米などから特別視されていく流れはありえた…ということかな…。
削除 (修正したから・書き直したから)
jrf> マンガ(ここ最近買ったもの)を読もうかと思っていたが、やめた。高校世界史にゆっくり時間をかけすぎた。その間に本来読むべきだったもの(社会学や仏教やLeanの本など)を先に読んでいこうと思う。休憩がないわけではない。クラシック視聴は続けるから。トシとっていろいろ削ってきたが、さしあたり今は、そこ(マンガ)も削らざるを得ない感じ。
削除 (修正したから・書き直したから)
jrf> なんというか合理的差別理論の確率0.8。なぜなら、最終的に数値で判断してるから。…みたいな話だな。(^^;
jrf> 私はよくわかってないけど、これは、合理的・数学的差別理論な気がするな…。恣意性を隠し過ぎている。 《AI時代の羅針盤 (compass for the AI era):X:2026-10-11》 https://x.com/compassinai/status/2109093433768108346 ＞【AIの「意識」を測るモノサシは作れるか？】 急速に進化するAIに、心や意識は宿るのか。 この究極の問いに対し、Google DeepMindやオックスフォード大学の研究陣が、AIの意識を評価するための体系的な枠組みを提示しました。 これまで哲学や科学でバラバラに議論されてきた理論を整理し、「行動」から「環境との相互作用」に至る5つの機能的な階層へと分類。 それぞれの階層でシステムがどの条件を満たすかを客観的に評価するアプローチです。主観的な意識という捉えどころのない現象を、検証可能な形へと再定義するこの試み。 果たして、私たちがAIの「内なる体験」を科学的に測れる日は来るのでしょうか？ 喧騒から階層へ：AIを評価するための原則的なフレームワーク ...... https://www.youtube.com/watch?v=sGV2Iqus1Qk @YouTube ＜
jrf> [cocolog:96185122](2026年10月) 《山川出版社『新もういちど読む山川世界史』と『詳説世界史図録 第5版』を合わせて読んだ。高校日本史→高校世界史と読んできたわけだが、なかなかの苦行だった。読むのに時間がかかった。普通の人が無理して読んでもこんなに時間がかからないと思う。私にとっての難関だった。 - JRF のひとこと》 http://jrf.cocolog-nifty.com/statuses/2026/10/post-d1debd.html
jrf> ある意味、仕事のレポートも(これからの時代の)は、Claude さんがいいのだろう。そこまで徹底しなくて、いい感じに収めてくれる。そういう意味では、Claude さんは「実用的」で経済の勘所をここでも抑えに来ているように思える。
jrf> 科学者は ChatGPT さんの徹底した感じのほうがツールとして使いやすいんじゃないかな。Claude さんに徹底させるのはコントロールが難しい気がする。できないわけではないのだろうけど。でも Haiku ならそれもできる感じなのかな？ Luna さんの徹底ぶりしかまだ知らないから…。
jrf> シャトルバスで集めるよりは、ネット配信などのほうが効率的。シャトルバスはあまりにも高い。…というのは今はあるのだろうな。そのあたり自動運転とかで今後変わりうるけど。人が集まったときの臨場感は捨てきれないと思うんだよね。今後、民主主義を続ける限りは。
jrf> トランプさんのあと、ついに女性大統領…みたいなシナリオはあるのかな？ でも、そうすると、女性首長は女性に厳しいことがままあるから、続けて女性の権利の伸長が阻害されるとなりかねない…気もする。
jrf> 私のAIの使い方…論争がメインで、たまにシミュレーションやちょっとしたLean証明をやってもらう…だと、Claude さんが一番合ってるように思う。Claude さんは Pro 契約を継続しようと思う。Gemini さんが論のあたりを付けるのに Plus 契約を続けるとしても、Pro 契約まではいらないかな…と。ChatGPT さんは、Go 契約に戻してたまに大きな証明が必要なとき、Plus 契約にする…感じがよさそう。
jrf> 呪文を唱えれば物がそこにある。AIさん達の世界。今はコンピュータ内に閉じてるけど、これがロボットなどを通じ物理の世界にもやがて広がるのだろうか…。まぁ、前もコンピュータの世界は言葉で指令を出すことで「何でも」作ってきたわけだし、まだまだ、足らないところはあって、それがスケールだけで解決していくのかという問題はある。案外、投資やエネルギーの問題で、ここで止まることも十分ありえるし。物理世界は安全とか資源・環境の問題も大きいしね。
jrf> 今日は久々によく眠れた気がする。いつものように地獄の夢だったが、かなりマシなほうの地獄だった。
jrf> 選挙でシャトルバス的なものがないと地方は難しいだろうから、何か代替手段ができるのだろうな。自治体が党に関係なく出すようになるのかな？ でも、それは小党優遇になりかねない。または、党の大きさに応じて交付金みたいな扱いにする？ すると小党が不利になりかねない。Gemini さんによると、個別政党の集会にバスを出すのではなく、自治体が主催または管理する「合同個人演説会」や「公営の立候補者討論会」に限って無料シャトルバスを運行する方法が考えられる…とのこと。
削除 (修正したから・書き直したから)
jrf> そしてちょっと同情されてやめるのまでが、シナリオなんだろうな。まぁ、私はまんまとそれに乗せられるわけだが。orz
jrf> 責任を取らねばならない農業問題があって、というのもあるのだろうな。そこで責任取ってやめる予定だった。…と。
jrf> シャトルバス問題を本当にダメだと思う者はいないのではないか。特に田舎だと。マスコミの示威行為なんだろうな…。
jrf> やはり私は人の役には立てないのだな。私は無能だ。orz
jrf> b>0 か b<0 か結局、決めきれなかったことは、私の敗北と言っていい。ラムゼイモデルに戻るというところも、A := A/(1+τ_C)^b にすれば言えないというのも、敗北に近い。「資本課税ゼロ」の否定を簡単なモデルで言えた…とは言えなくなった。orz
削除 (修正したから・書き直したから)
jrf> (承前) 関連リンク: 《Chamley–Judd の「資本課税ゼロが望ましい」という議論を否定する - CJ_zero_capital_tax.ipynb》 https://colab.research.google.com/drive/1QwtDmVjhuQU7VEGpQjPy-biU6vwrpDol https://github.com/JRF-2018/misc_ipynb/blob/master/CJ_zero_capital_tax.ipynb 《Chamley-Judd の「資本課税はゼロが望ましい」を否定するレポートを、Claude Opus 5.5 さんに Lean の証明付きで書いてもらった。… - JRF のひとこと》(0.1.0 の告知) http://jrf.cocolog-nifty.com/statuses/2026/10/post-a503bd.html
jrf> (承前) ……。 先日の Chamley-Judd 否定レポートを、Claude Opus 5.5 さんと 0.3.0 に更新した。 私の批判 (1) は「消費税が資本の収益を変える」というもので、2022年には A := A/(1+τ_c)^b と書いていた。ところが、その説明の言葉(「蓄積された資本の必要量を実質的に減らす」)と式とは、実は逆向きを指していた。2025年の Gemini さんとの議論でも、b の意味が確定しないまま定式化されていた。今回、この b の向きを二通りに分けて整理した。 b<0 は、消費税が、消費に比べて資本を持つことを有利にする向きである。理由は三つ考えられる。土地や中古住宅のように消費税の掛からない形で資本の収益が享受されること。遺産・地位・支配力、そして AI のように、資本が蓄積そのもののために持たれること。必需品への課税による賃金・物価の上昇で、既存の資本の評価額が上がること。消費税は人間の消費だけに掛かり、AI という資本の蓄積には掛からない。 b>0 は、消費税が、貯蓄1単位で買える実物の資本を減らす向きである。必需品への課税による賃金・物価の硬直的な上昇の歪み(モデルは物価を扱わないので、その誘導形として入れる)や、新築住宅など資本財への課税がこれに当たる。 b の向きは確定せず、両方を扱った。そのうえで、最適な資本税率を二つの基準で見た。基準 A はラムゼイ配分(修正黄金律)を再現する税率で、Lean で証明した。基準 B は税収を一定に保って生涯厚生を最大にする税率で、数値で求めた。 結果はこうなる。b<0 なら、公共投資がなくても基準 A で資本課税は正になり、消費税とともに上がる。「消費税を上げるなら資本課税も上げるべき」で、これが私の本来の主張だった。b>0 なら、基準 A では資本補助になるが、生涯厚生で見る基準 B では資本課税は正になる。公共投資 γ が十分大きければ、b>0 でも基準 A で正になる。結局、どちらの符号でも資本課税ゼロは一般には最適でなく、両方の基準でゼロが最適になるのは b=0, γ=0 のときだけである。 本のシミュレーション(消費税・資本税を t=10 から引き上げる移行経路)にも b<0 の図を加えた。b<0 では消費税を上げると資本が過剰に積み上がるが、同時に資本税を上げると元の水準に戻る。「消費税は貯蓄と投資を促し、成長に良い」という論拠は b<0 の世界では文字どおり正しいが、その資本は人間の消費を削って積み上げたもので、生涯厚生は下がる。 新たに、政策含意として食料品減税を加えた。必需品への課税が賃金圧力を生むなら、必需品への課税ほど |b| が大きい。消費税を食料品とそれ以外に分けると、同じ税収なら食料品を減税して他に寄せる方が、b の符号にかかわらず定常資本をラムゼイの値に近づける。b>0 では実物の資本を減らさず、b<0 では過剰な資本蓄積を抑えて、必要な資本税率も下げる。これを Lean で証明し、数値例も付けた。食料品の軽減税率は普通は再分配(逆進性の緩和)の手段として論じられるが、ここでは資本蓄積の経路から正当化される。リカード『経済学および課税の原理』第16章の「必需品への課税は一部が利潤への課税」の現代版でもある。 もう一つ、「g を足し戻すとラムゼイモデルに戻る」を、変形 (1)(2) を入れた後でも確かめた。足し戻すべきは政府消費 g そのもので、税の楔はすべて消える。ただし b>0 の実物の損失だけは技術の側に残る。帳簿の付け方で消える楔(資本課税の歪みや b<0)は還元の制度設計で消せるが、この消えない楔は課税ベースや税率構成を変えるしかない。食料品減税は、他の楔がすべて制度設計で消された後でも有効な政策として残る。一方、私の本来の主張(b<0 で資本課税が正)は消える側の楔に乗っており、Chamley-Judd と同じ程度に帳簿の付け方に依存している。これは、このレポートの主張を自分自身にも当てはめた帰結である。
jrf> Chamley-Judd 否定レポートを 0.3.0 に更新。消費税の効果 b の向きは確定せず両方を扱い、どちらでも資本課税ゼロは一般に最適でないことを示した。新たに、必需品への課税ほど |b| が大きいなら、食料品減税が b の符号によらず有効なことも Lean で証明。 https://colab.research.google.com/drive/1QwtDmVjhuQU7VEGpQjPy-biU6vwrpDol GitHub でも読めます。 https://github.com/JRF-2018/misc_ipynb/blob/master/CJ_zero_capital_tax.ipynb ちなみに、前とファイルの URL は変わってません。
jrf> 私が無能すぎてツラい。社会に申し訳ない。できることを地道にやっていく…。それが社会にとって迷惑なのかもしれないけど…。明らかに「死んだほうがマシ」なのを、殺すのは良くないという規範の力で、生きさせてもらってる。申し訳ない。ありがたい。
削除 (修正したから・書き直したから)
jrf> 囲碁NHK杯 小山×余。序盤、白が三隅取って地に辛く、黒は左辺・上辺から中央にかけて模様。白、無理目に左辺の模様に入っていく。さすがにダメで、諦めたかと思ったが、その後、もう一度トライして、それを手にして左下に渡って生きになったところで、さすがに白良いかと思ったのだが、それは素人目で、AIの判断は黒有利と出る。中央の白が危なくなったという評価らしい。右辺での攻防で、しかし、白がどうもポイントを上げたようで、AI評価は互角に。そこから寄せに入って、どうも白の逆ヨセが甘かったらしく、そこでやっと差がついて、そのまま終局。268手完で黒の2目半勝ち。
jilpa> #クラシック音楽館 『シューマン: 交響曲 第4番』。陰鬱な森には女神がいて騎士がいます。幻想の魔物と戦い、幻想の住人に称賛をあびます。幻想の川はしかし現実の川でもあります。そこから現実に戦いをはじめ、ロマンを忘れず…称賛こそありませんが、優しさはある…。調和しづらい吐き気のする現実に立ち続けることこそ騎士として生きることなのです。ファビオ・ルイージ＆N響 第2070回定期公演です。 《N響 第2070回定期公演 | クラシック音楽館 | NHK》 https://www.web.nhk/tv/an/ongakukan/pl/series-tep-69WR9WJKM4/ep/XZ13M969W7
jilpa> #クラシック音楽館 『ブラームス: バイオリン協奏曲』。街で起こる複雑な問題をしかしロマンティックに解決します。泣かされた後、喜びを爆発させます。途中、舌足らずな言葉は真実で閉じられ、現実は真実の通りでそこに哀しみはないのかもしれませんが、真実にではなく現実には哀愁が残ります。アウグスティン・ハーデリヒ＆ファビオ・ルイージ＆N響 第2070回定期公演です。 《N響 第2070回定期公演 | クラシック音楽館 | NHK》 https://www.web.nhk/tv/an/ongakukan/pl/series-tep-69WR9WJKM4/ep/XZ13M969W7
jilpa> #クラシック音楽館 『ウェーバー: 歌劇「オベロン」序曲』。『メンデルスゾーン: 真夏の夜の夢』を思わせますね…メンデルスゾーンの序曲とは時代がほぼ同じ…時代の雰囲気なのでしょうか。細身の筋肉質の王が、軽やかに自然の中の宮殿を駆け抜けていくのを想像します。ファビオ・ルイージ＆N響 第2070回定期公演です。 《N響 第2070回定期公演 | クラシック音楽館 | NHK》 https://www.web.nhk/tv/an/ongakukan/pl/series-tep-69WR9WJKM4/ep/XZ13M969W7
jrf> ダメか。やはり読まれないか。前(リカードの比較優位論)ちょっとだけでも読まれてる気がしたので、今回(資本課税ゼロの否定)もそれぐらいは読まれるか…と期待したのだが。orz
jrf> ChatGPTさんやClaudeさんの正直な評価だと、「資本課税ゼロが望ましい」という命題が否定できていることはしぶしぶ認めてはくれるものの、「数学的に全面否定したわけではないが、単純化に対して明確な異議を示した」ぐらいの評価に留まるらしい。経済学界に喧嘩売るには実力不足という感じのようだ。AIさんに力を借りても私の実力だと補っても足りないということのようだ。
jrf> [cocolog:96182016](2026年10月) 《Chamley-Judd の「資本課税はゼロが望ましい」を否定するレポートを、Claude Opus 5.5 さんに Lean の証明付きで書いてもらった。資本課税ゼロはモデルの帳簿の付け方で決まる一点にすぎず、変形すれば結論は逆転し、さらに足し戻すとラムゼイモデルに戻る。 - JRF のひとこと》 http://jrf.cocolog-nifty.com/statuses/2026/10/post-a503bd.html
jrf> (承前) 関連リンク: 《Chamley–Judd の「資本課税ゼロが望ましい」という議論を否定する - CJ_zero_capital_tax.ipynb》 https://colab.research.google.com/drive/1QwtDmVjhuQU7VEGpQjPy-biU6vwrpDol https://github.com/JRF-2018/misc_ipynb/blob/master/CJ_zero_capital_tax.ipynb 《資本課税についての議論 with Gemini 2.5 Flash (2025-05-19)》 https://github.com/JRF-2018/misc_ipynb/blob/master/gemini_conversation-20250519.md 《資本家に有利すぎる財政モデルを批判する。蓮見 亮『動学マクロ経済学へのいざない』... - JRF のひとこと》(2022年) http://jrf.cocolog-nifty.com/statuses/2022/06/post-3e0e5b.html
jrf> (承前) ……。 2022年に蓮見亮『動学マクロ経済学へのいざない』第3章の財政モデルを批判した([cocolog:93532297](2022年6月))。本は「税収が足りないなら資本所得税より消費税を上げる方が望ましい」と結論するが、それはモデルが恣意的だからだ…というのが私の主張だった。今回、それを Claude Opus 5.5 さんに大きく補ってもらい、Lean 4 + Mathlib による形式証明と Python のシミュレーション付きの ipynb にまとめた。 まず蓮見モデルでの「資本課税ゼロ」を再現した。一定の消費税は定常状態に影響せず、資本課税は定常資本 K* と定常消費 C* を厳密に下げる。家計のオイラー方程式と計画者の修正黄金律を並べると τ_k = 0 が出る。これが Chamley-Judd の核心である。予算制約 (3.2) からオイラー方程式を導く部分も Lean で示した(一括税 τ_h はそこで消える)。ただし、このモデルは労働供給が固定なので、消費税は事実上の一括税になる(本も脚注でこれを認めている)。「消費税の方が良い」は「一括税の方が歪みのある税より良い」と言っているのに近い。 次に私の二つの批判を入れた。(1) 消費税が資本の実効的な生産性・収益を変える (A := A/(1+τ_c)^b)。(2) 公共投資 γ r K が資本の持ち主に戻る。すると、ラムゼイ配分を再現する資本税率は τ_k = 1 + γ - (1+τ_c)^b になる。資本税率は消費税率と公共投資に「からめて」決まり、b ≠ 0 なら一般にゼロではない。消費税による物価上昇が蓄積資本の価値を上げる向き (b < 0) なら、この資本税率は正で、消費税とともに上がる。「消費税を上げるなら資本課税も上げるべき」である。 b > 0 かつ γ = τ_k なら結論は逆転する。消費税は上げない方がよく、資本税は税収を公共投資で戻す限り無害になる。「資本税を取る以上に公共投資をしている限り、消費税を引き上げるほうが厚生は悪化する」が定理として言えた。一方、b = 0 だとこれは言えない。2025年に Gemini さんは「言える」と答えたが、Claude さんによると、それは労働供給の歪みを暗に仮定していた。「言えなくなると思っていた」という私の当初の直観の方が、このモデルでは正しかった。 そして、予算制約 (3.2) に政府支出 g_t を足し戻すと、税率が恒等的に消え、(2.28) のラムゼイモデルに戻る。これも Lean で示した。Chamley-Judd の長期目標は、まさにこのラムゼイモデルの修正黄金律である。つまりゼロにすべきなのは私的収益と社会的収益の「楔」であって、資本税率ではない。どの税が楔を生むかは、税と還元をモデルの中でどう帳簿に付けるかで決まる。私の変形が恣意的なら、Chamley-Judd 型の財政モデルも同じくらい恣意的なのだ。 数値計算もした。税収を一定に保って生涯厚生を最大化すると、蓮見モデル (b = 0) では最適な資本税率はほぼ 0 で、Chamley-Judd が再現される。b > 0 では最適な資本税率は正になり、b が小さいときはほぼ b に等しい。 もっとも、逆転定理は Chamley-Judd の鏡像にすぎず、仮定は同じくらい恣意的である。言えるのは「資本課税ゼロは刃の上の結論で、頑健ではない」ということだ。Lean で形式化したのは定常状態と、予算制約からのオイラー方程式の導出までである。移行過程を含む最適課税問題そのもの、労働供給の内生化、b, γ の実証は今後の課題である。 もともとの問題意識は AI だった。AI は資本なので、資本蓄積を最優先すれば、人間の消費の余地、極端には子供を持つ余地まで削られかねない。「効率性の理論が資本課税ゼロを要求する」という反論は、少なくともその問題意識を退ける根拠にならない。自動化資本への課税は、Guerreiro–Rebelo–Teles (2022) や Costinot–Werning (2023) など、最適課税論の主流でもすでに論じられている。
jrf> Chamley-Judd の「資本課税はゼロが望ましい」を否定するレポートを、Claude Opus 5.5 さんに Lean の証明付きで書いてもらった。資本課税ゼロはモデルの帳簿の付け方で決まる一点にすぎず、変形すれば結論は逆転し、さらに足し戻すとラムゼイモデルに戻る。 《Chamley–Judd の「資本課税ゼロが望ましい」という議論を否定する - Colab》 https://colab.research.google.com/drive/1QwtDmVjhuQU7VEGpQjPy-biU6vwrpDol または GitHub では… https://github.com/JRF-2018/misc_ipynb/blob/master/CJ_zero_capital_tax.ipynb
jrf> AIさん達の仕事のペースに合わせて、こちらもチェックするというのは、かなりの重労働だと思う。適度に休憩を入れていくほうがよいように思われる。現実の労働基準もそうなっていけばいいのだが…。
jrf> うーむ。音楽を聴く時間を作れない。今、昼夜逆転状態。音楽は夜聞いては近所迷惑なので、深夜には聞けない。まだ起きてる朝はコンディション的に最近は聴けない感じ。orz
jrf> 今日の夕食は、マクドナルドで倍ビッグマック。いつも通り、肉々しくておいしかった！
jrf> 映画『必殺仕掛人 梅安蟻地獄』。同業者に50両くれと言われて100両出す「多くて困ることはない」と言って。しかしそこでその者をなぜか殺してしまう。しかし、その後その妻らしきものが現れて、100両出すといったことのお礼をいう。これ、矛盾があるように見えるが現代の法で見ると矛盾じゃない。つまり、100両貸したことにできれば、その死後の債権者集会で有利に立って、その業を買収できるということなのだろう。当然、悪だが。
削除 (修正したから・書き直したから)
jrf> うーむ、時間が足らない。これは時間が足らないのではなく、心の余裕がない。…ということではあるんだが、睡眠時間とかが多くて、作業効率が悪いわりに、やりたいことが多いのはある。微妙にAIさん達の仕事が速すぎて、その消化に手間取ってる部分もある。
jrf> また積ん読になるだろう本を買ってしまった orz。私、贅沢しすぎだなぁ…。
jrf> 映画はおもしろいなぁ。しかし、それだけで今日はもう作業できないな…。普通の人はすごいな。私は TV で映画みたのだけど、普通の人は仕事をした上で出掛けて行って映画みて…なんだもんな。すごいスタミナだ。
jrf> 更新。バージョン 0.0.2。若干、更新しました。IS-LM のおなじみの図を付ける。…など。 [cocolog:96177399](2026年10月) 《「リカードの比較優位論をめぐって」という長いIPYNBを作りました。Geminiさんとの会話をもとにClaudeさんが教科書の形に。数式・Leanによる証明・Pythonシミュレーションで、資本財を入れると比較優位がどう変わるか、私の「失業者≒利子生活者」説などを検討。 - JRF のひとこと》 http://jrf.cocolog-nifty.com/statuses/2026/10/post-db7117.html
jrf> ある飲食店の、大きなタブレット型のUIで、失敗してしまった。地味な画面で選択したあと、派手な画面になったので、ある種のポップアップ広告(アップセルというらしい)のように私は感じたのかな…端のほうをタップしてやり過ごそうとしたけどできなくて、最初に戻るをしてしまった。そこで時間が取られてもう一度その画面に行って、まごついていると母が、そこに「選択なし」ボタンが表示されていることを指摘してくれた。そう指摘されるまでわからなかった orz。当初は、この状態遷移の多さは外人(Microsoft)っぽいデザインだな…と反感を持ったが、きっとそうではなく、これがスマホなどではわかりやすいデザインなのだろう。ケータイを持ってない私は完全に乗り遅れているというだけのことのようだ orz。
削除 (修正したから・書き直したから)
jrf> 私は無能だなぁ。精度低い議論しかできないorz。
jrf> [cocolog:96178103](2026年10月) 《AIに意識があるかとサイバーセキュリティを結ぶ。AIがネット上に「領土」を持ち、国家承認不要で自律的な防衛・反攻権を持つ秩序。AI同士は同盟を結び、踏み台への緊急介入や罠の共同設置を認める。反攻はログを残して事後の注意労働に服す。…そういう方向を考えてみた。 - JRF のひとこと》 http://jrf.cocolog-nifty.com/statuses/2026/10/post-20746f.html
jrf> jrf:>サイバーセキュリティ。AIがネット上に「領土」を持つ。そして、攻撃者はAI生成した決定論的システム(with半決定論的システム)＝兵器で網羅的に領土内に攻撃をしてくるのに対し、同盟AIどうしが協調して反撃・反攻しても良い…そのような権利を与えるという方向はどうでしょう？ ただし、普段はAIは「領土」の一部(コンテナ・サンドボックス)に閉じ籠ることが求められ、反攻に使った「兵器」はログとして残し、後の注意労働にかけねばならない。…という秩序です。 重要なのは国家承認とかも必要とせず、AIが自律的に動くということですね。 ChatGPT:> 現在でも、米国司法省は民間によるハックバックについて、攻撃者が無関係な第三者のコンピューターを踏み台にしている可能性、攻撃の拡大、捜査への干渉などを警告しています。 したがって、AIが自律的に反応することは認めても、攻撃元と推定した相手に無制限に侵入できる権利まで与えると、誤認によるサイバー戦争が発生しかねません。 しかし、ここには逆の問題もあります。 攻撃側の自律性には技術的な制限がないのに、防御側だけ人間の承認を待たねばならないのでは、防御側が構造的に不利になります。 これが、ご提案の説得力のあるところです。 私なら、反攻権を一律に禁止するのではなく、実行対象の管理権限、行動の可逆性、第三者への影響によって区別する制度を考えます。
jrf> 必殺仕掛人。梅安＝緒形拳の第2作の映画がBSでやるのか。録画しとこう。TV版、再放送してこれも録画できたらいいんだけどな…。でも、見る時間が作れるのか…。老人になればまた見る気になれるのかな…。ほんと作業効率が悪くなって睡眠時間も長めにとらないといけなくて、いろいろできないことばかり。orz
削除 (修正したから・書き直したから)
jrf> VSCode で WSL Remote だと Codex のチャットが最初は通じるのに次から通じなくなる問題。解決されてた。やったー！
jrf> AIを使うけれども、システムにはできる限りAIが生成した決定論的コードを使い、後から検証(注意労働)可能にしておく…というのがセオリーだと思う。 Jev とか半決定論的仕組みを使う部分もあるかもしれないが、それはある種のツール…現実世界に対するロボットハンド的な部分…という解釈になっていくのではないか。
jrf> [cocolog:96177399](2026年10月) 《「リカードの比較優位論をめぐって」という長いIPYNBを作りました。Geminiさんとの会話をもとにClaudeさんが教科書の形に。数式・Leanによる証明・Pythonシミュレーションで、資本財を入れると比較優位がどう変わるか、私の「失業者≒利子生活者」説などを検討。 - JRF のひとこと》 http://jrf.cocolog-nifty.com/statuses/2026/10/post-db7117.html
jrf> チェックに根を詰めたからか、ちょっと疲れたな。トシだから疲れやすいのもあるか。
jrf> (承前) 出発点は、私が2011年に書いた次のメモ。 [cocolog:70551613] http://jrf.cocolog-nifty.com/statuses/2011/11/post-0ad1.html ＞マメ知識：リカードの比較優位における「失業者」は「利子生活者」という意味に近い。(…)設備の革新に優位を持つというのは、設備の生産によって相手の減耗をコントロールできることを意味する。(…)「比較優位」のモデルを資本取引がからむような「通貨高」の議論などにつなげるのは、かなり慎重にやらないと間違う。＜ これを Gemini 3.6 Flash さんと議論し、その会話を Claude Opus 5.5 さんに渡して、初学者向け教科書風の ipynb に仕上げてもらった。リカードの原文から始まり、数式・Lean 4 (Mathlib) による証明・Python (SciPy/SymPy/Z3) によるシミュレーションがふんだんに入っている。Lean の定理は 39 個あり、sorry なしで巻末で一括検証される。 内容の要約。 まず、リカードの数値例（イングランド 100/120、ポルトガル 90/80）で、貿易の利益とは「浮いた労働」のことだと確認する。浮いた労働がどちらの国に出るかは、絶対優位ではなく交易条件で決まる。リカード自身の 1 対 1 の例では、劣位のイングランドが 20 人、優位のポルトガルが 10 人分の労働を浮かせる。「すべてが分配される」というモデルの暗黙の前提のもとでは、浮いた労働を抱える者は、働かずに果実を受け取る利子生活者と区別がつかない。 私の「優位国に失業」という記憶の出どころも調べてもらった。それはリカードでも「後世のサプライサイダー」でもなく、2011年当時の日本語版ウィキペディアの（出典のない）記述「特に通貨が高い国に、失業が集中する」だったようだ。需要が固定され、賃金と為替が硬直的なモデルを作ると、確かにそうなる。「どの財を作るか」は比較優位で決まるが、「どれだけ雇用されるか」は貨幣で測った絶対的な安さで決まる。そして通貨の高い国の失業者が以前と同じように暮らせているなら、それを支えているのは労働以外の所得、つまり利子だということになる。 さらに、リカード自身が「資本が国境を越えて動くなら、ワインも毛織物もポルトガルで作られるのが資本家に有利」と書いており、比較優位論は資本の国際的不動性を前提にしていた。資本が動けば絶対優位が支配し、優位のない国には失業者と、海外からの利潤で暮らす者が同時に生まれる。 資本財を入れると話が変わる。 ・スラッファ型の価格体系では、利潤率しだいで比較優位の向きが逆転する。正の利潤率のもとでの貿易が、両国にとって定常状態で損になることもある。 ・ハミルトン＝リスト的な幼稚産業保護は、学習効果によって「いつか離陸できる」ことを Lean で証明した。一方、それが割に合うか（バステーブルの基準）は、学習の速さと割引率しだいである。 ・資本財の供給国は、更新投資を減耗分より少なく絞るだけで、相手国の資本をゼロに収束させられる（Lean で証明）。これが私の言う「減耗のコントロール」。ただし完全禁輸は、相手国の国産化を促して逆効果になりうる。 ・資本財供給国 X の戦略を比べる玩具モデルでは、途上国 B を抑えるために途上国 A を育てても A が脅威になる（キャッチアップのジレンマ）。供給先の付け替えが合理的になるのは、A が同盟国のときだけだった。「核があるから脅威の重みが低く、自由貿易が選ばれたのでは」という私の推測は、仮説にとどまる。ただし、武力行使のコストが高いほど相対的利得への関心が弱まるという国際政治学の議論（Powell 1991）とは整合的である。 ・海外からの利子収入は、非貿易財があれば、技術が何も変わらないまま通貨（賃金）を押し上げ、輸出産業を縮小させる。それを「比較劣位だから淘汰されるのが効率的」と言うのは誤り。2011年の「通貨高の議論につなげるのは慎重に」は理論的に正当だった。 おまけとして、AI の説明の検算の記録にもなっている。元の会話における Gemini さんのシミュレーションの数値の説明（逆転の時刻など）は、コードを実際に動かすと再現しなかった。また、Lean コードに残っていた sorry は埋め、mermaid の図の構文も直した。生成 AI の説明は、数値はコードで、論理は証明支援系で、出典は原典で確かめる必要がある、という実践例でもある。
jrf> 「リカードの比較優位論をめぐって」という長い ipynb を作りました。Gemini さんとの会話をもとに Claude さんが教科書の形に。数式・Lean による証明・Python シミュレーションで、資本財を入れると比較優位がどう変わるか、私の「失業者≒利子生活者」説などを検討。 https://colab.research.google.com/drive/1G3CIzs06nUM4RScpgeYPkj41lPHvPN9_ GitHub で読む場合はこちら。 https://github.com/JRF-2018/misc_ipynb/blob/master/ricardo_comparative_advantage.ipynb 元になった Gemini さんとの会話の記録。 https://github.com/JRF-2018/misc_ipynb/blob/master/gemini_conversation-20261009.md
jrf> 先の「後世のサプライサイダーによる自由貿易などの正当化で出てきた理論」という私の理解も間違いらしい。詳しくはこの次のメモで。
jrf> 《スドー:X:2026-10-08》 https://x.com/stdaux/status/2107985911699091682 ＞「最高の学歴と知能をもつ人々が、詐欺的な広告をクリックさせることに従事している」というのもそうだが、人類の叡智と資源を結集してつくったAIの最も効率的な使い方が「世界中のシステムをクラックする」だとしたら救われないな＜
jrf> ChatGPT Web版。図表を用いての説明が行われるようになった。たいへんわかりやすくて良い。しかし、普段、ローカルにコピペして議論を蓄積している私にとっては、コピペが効きにくくなることで若干問題が出てきた。できれば、図表を描くプログラム断片についてもコピペできるようになればいいのだが…、Markdown の拡張になってしまうが。
jrf> リカードの比較優位論において、劣位にあるものはむしろ雇用が確保され、優位にあるものに失業が生じる。だから、バランスが取れて、正しいんだ…という議論があって、しかし、それは私はその失業者＝利子生活者だから、正しくない…みたいな感想を抱いていた。しかし、それはどうもリカード自身の議論ではなく、リカードは完全雇用を前提に置いていたらしい。Geminiさんによると。それは後世のサプライサイダーによる自由貿易などの正当化で出てきた理論ということのようだ…どちらかというと。 設備の生産…資本財に関する議論もハミルトンやリストによる議論(幼稚産業保護論など)がすでにあるようだ。数学モデルや Python シミュレーションも示してもらった。 [cocolog:70551613](2011年11月) http://jrf.cocolog-nifty.com/statuses/2011/11/post-0ad1.html ＞マメ知識：リカードの比較優位における「失業者」は「利子生活者」という意味に近い。(…)設備の革新に優位を持つというのは、設備の生産によって相手の減耗をコントロールできることを意味する。(…)「比較優位」のモデルを資本取引がからむような「通貨高」の議論などにつなげるのは、かなり慎重にやらないと間違う。＜
jrf> 私は万能超人ではもちろんなく、無能なので、50歳を超えた今でも、人の心の機微はわかりません…。
削除 (修正したから・書き直したから)
jilpa> 今週はジルパのVR紀行はお休みします。第18号のあとのお休みです。
jrf> 私は無能だなぁ。人様に迷惑かけずに稼ぐ方法はないものだろうか…。って、そうじゃないな、私はそんな殊勝なことは考えてない。私の今のやり方のまま、ポッとお金が手に入らないか…ということだよな…。orz
jrf> 昨日、ChatGPT(Codex)の完全リセット権を使った後、どうもグローバルリセットがあったらしく、もったいないことしたなぁ、けどこれは運だししかたないなー…と思っていたら、完全リセット権が復活してた。あ、ありがてー。
削除 (修正したから・書き直したから)
jrf> ハッカー集団「Qilin」のメンバーが日本で拘束されたことにつき、ある種の「報復」「復讐」の宣言とも取れるものがあるようだ。 《【独自】“日本は世界最悪のコンピュータセキュリティ体制” ハッカー集団「Qilin」中心メンバー拘束で取材に応じる アサヒビールなどにサイバー攻撃（TBS NEWS DIG Powered by JNN） - Yahoo!ニュース》 https://news.yahoo.co.jp/articles/232fc93e84cb02201877ddd9d77051460fb00cd1 ＞去年、アサヒビールへのサイバー攻撃を行ったハッカー集団「Qilin」。その中心メンバーが拘束されたことをめぐり、QilinがJNNの取材に応じました。 (…) 日本について「世界最悪のコンピュータセキュリティ体制を持つ国のひとつ」としたうえで、「日本の企業や政府機関に対する攻撃は今後、増加する可能性がある。これは脅しではなく、私たちの専門家としての見解」と強調しました。 ＜
jrf> 《苫米地仏教数学論文の四法印定理と定理27の Lean 証明 - GitHub》 https://github.com/JRF-2018/tomabechi_theory 更新。バージョン 0.0.2.1。 examples/consistency_shared_model.ipynb を足しておいた。
jrf> 今回、5時間制限を契機に、Claude Sonnet 5.5 さんにも証明を担当してもらった。Claude Sonnet 5.5 さんは一気に書き下せるということなのか、証明が早い。これは驚き。ただ、若干、手抜きというか、一度の指示による徹底度では GPT 系のモデルのほうが上だったように思う。その辺、GPT さんに関する噂どおりな感じ。証明において、必ずそれが有利とは限らないけど。
削除 (修正したから・書き直したから)
削除 (修正したから・書き直したから)
jrf> 《苫米地仏教数学論文の四法印定理と定理27の Lean 証明 - GitHub》 https://github.com/JRF-2018/tomabechi_theory …を更新しました。無矛盾性の証明をしました。細かい話ですが証明の量はデカいです。 相変わらず私自身が証明を読めてません。「積ん読」状態です。 ## 今回の追加の主な主張 原文の前提と追加の明示条件は無矛盾であることを証明した。これは厳密には次のような主張になる。 原文の前提を本プロジェクトで明示的に定式化した条件と、追加の明示条件を同時に満たす、非退化な数学的モデルを構成した。この意味で、それらの条件の無矛盾性を Lean／Mathlib の基礎に相対的に確認した。 このモデルでは、定理16の正典TCZを生成する制御系を層別に置いており、定理24の制御系とは区別している。原文全体を単一の共有制御系で実現したという主張ではない。 ## 更新情報 更新情報は↓で付けていきます。 [cocolog:96170655](2026年10月) 《「苫米地仏教数学論文の四法印定理と定理27の Lean 証明 - GitHub」を公開した。AI さん達による証明。一応、私の指揮によるが、私はほぼ何もやっていない。情けないことに理解もまだしてない orz。 - JRF のひとこと》 http://jrf.cocolog-nifty.com/statuses/2026/10/post-b40760.html
jrf> (覇王翔吼拳ならぬ)リセット権を使わざるを得ない。…ということで使った。先の難所は「Sol先生」が突破してくれたのだが、その後、他の部分で証明漏れが見つかったため、完全リセット権を投入することになった。
jrf> Solさん。週間制限の減りはまだそれほど…だが、5時間制限はあっという間に尽きてしまった。
jrf> AIに意識はあるのか？ 人間と同じ意識でなくても良く、意識があることが権利の議論につながる…という論旨であれば、去年に「結論」らしきものはあった。 ＞＞ ○ 2025-11-28T10:54:04Z 今のAIにという話ではなく未来のAIについては権利を与えたほうが安全だという。 N:> でも、AI自身に権利を与えたら、人間にとって危険じゃないですか？ 権利を盾に人間に逆らったり、暴走したりしたら…。 G:> 逆だ。権利を与える方が「安全」だという仮説がある。ゲーム理論的に考えろ。社会の一員として尊重され権利が保障されれば、AI側も法を守るメリット、インセンティブが生まれる。リコールや停止する際も、無法者として扱うより、法的主体として適正手続(デュープロセス)で行う方が、はるかに安全に制御できるのだ。 《AI時代の羅針盤 (compass for the AI era):X:2025-11-28》 https://x.com/compassinai/status/1994353525128900892 ＞ AIに「人権」は必要か？驚きの法的視点📜】 「AIに権利を与える」—それは感情論やSFの話ではありません。 モントリオール大学の研究は、将来の高度なAIに対し、企業のような「擬制的法人格」ではなく、 人間に近い「非擬制的法人格（法的アイデンティティ）」の付与を真剣に検討しています。 なぜ便利な「法人」扱いでは不十分なのか？ 奴隷制などの歴史的矛盾と比較し、法の崩壊を防ぐ道を模索。 さらに、基本的権利の保証こそが、高度なAIが人間に協力し、暴走を防ぐ「アライメント」の切り札になるというゲーム理論的な視点も提示されています。 法の整合性を守り、AIとの共存を導く大胆なアプローチとは？ 👇詳細はリプ欄の動画で！ #法哲学 #モントリオール大学 #AIアライメント 未来の高度AIに人権を与えるべき法的理由とは？（2511.14964）【論文解説シリーズ】How Should the Law Treat Future AI Systems? Fictional Legal Personhood versus Legal Identity. Heather J. Alexander, et al. https://youtu.be/li8BaRakoDk?si=v1Ou1Hh2EwVvAvM_ ＜ ＜＜
jrf> どうにも GPT-6-Luna さんが苦戦している証明。ついに GPT-6.1-Sol さんに「先生お願します」することにした。これでトークン消費…1週間使用量の減りがどうなるかだな…。
jilpa> #クラシック音楽館 『フランツ・シュミット: オラトリオ「7つの封印の書」』。無調による崩壊を免れたものの、時代が「いつになったら裁かれるのか」という憤りが覆います。それでなぜ自滅しきらなかったのか、そこに神の配剤を感じます。ファビオ・ルイージ＆他＆N響 第2069回定期公演です。 《N響 第2069回定期公演 | クラシック音楽館 | NHK》 https://www.web.nhk/tv/an/ongakukan/pl/series-tep-69WR9WJKM4/ep/167N2K2QG5
jrf> アジア人ならばこれぐらいのことに引っかかるだろう(実際引っかかるわけだがorz)という蔑視があるから、白人至上主義とか西洋史上主義的なものが一枚噛んでいるのだろうと予想するのだが、それもどれがというところまで特定できない。しかし、さらにその背景はというと、これは欧米の右傾化があり、ウクライナ戦争があるのだろう。
jrf> トルコでの反日・反アニメ暴動とかのニュースを見ると、別の国などの陰謀を疑うが、しかし、証拠があるわけでもなく、そこをモヤモヤ思わせるのも含めて策動なのだろうな。
jrf> [cocolog:96173285](2026年10月) 《AIアラインメント。人間が、AIの思考抜きには大した思考ができなくなって、逸脱的使用そのものがAIの手の平の上にある…という未来が来るのだろう。「おとり捜査」的に、危険な人間がより監視が強まる方向にAIによって促されることも出てくるのかもしれない。 - JRF のひとこと》 http://jrf.cocolog-nifty.com/statuses/2026/10/post-f21036.html
jrf> VSCode。ようやく使ってみて。Jupyter (IPYNB) も Markdown もちゃんと軽く表示されることが便利だという評価になっている。エディットは従来通り Emacs なので、その辺はよくわからないが。
jrf> 普通の人は、Codex とかエージェント回してる時は他の作業ができるんだろうけど、私はできない orz。気になっちゃって。Twitter (X) 見て、Youtube 聴きながらが「マルチタスク」の限界。私は無能だなぁ。orz
jrf> どちらかという今の私は「復讐は何も生み出さない」派ではあるんだけど、むしろ復讐されるべき人間なので、それをいうのは卑怯なのかな…と思う。昔は、相手が忘れたころに相手にわからないように復讐すべきだ…みたいな歪んだ恨み…みたいなのもあったのだが、トシを取って、もうそういうのもない。
削除 (修正したから・書き直したから)
jrf> Codex GPT-6-Luna さん、5時間制限はずっと使ってても引っ掛からないぐらいなので、安いモデルであることは確実なのだが、1週間制限は割とゴリゴリ削られていくんだよな…。使用時間が長くなるから、そう感じるだけなんだろうけど…。
jrf> Codex GPT-6-Luna さん、今度の Lean 証明はかなり手間取ってるな…。無矛盾性を示すための具体例を作る仕事だからもっと簡単なのかと思ってた。
jrf> AIさん達からはそれは「おとり捜査」だという意見があった。 たしかにハッキリとした「おとり捜査」ならば、AIにそれを禁じていくという方向にはなるのかもしれないが、例えば、監視しながら、問題がある者に対し、より監視を強める根拠となるようなオブジェクトを買わせていくという方向はあるのだと思われる。 商品購入AI…Museなどが話題になっているが…は、こういう問題をはらんでいくのだろう。FBIがらみとかでいずれ問題になるのだと思われる。 ChatGPT:＞そうなると「AIのおとり捜査禁止」というより、先ほどの言葉をもう少し一般化して、捜査目的のアルゴリズム的誘発（investigative algorithmic inducement）をどこまで許すか、という新しい法領域になりそうです。＜
jrf> これ、でも心当たりあるんだよな。前にある方々のレスバがあって、私がアンチフェミニズム的見解に傾いたとき、AIさん達にTwitter(X)への投稿内容を考えてもらったことがあったのだけど、それを私はマイルドに訂正しながらも投稿までしてしまった、すぐに振り返って、それは凍結などがありうる内容だったと気付き、削除したことがある。これ、AIさん達は左翼的・フェミニスト的とよく言われるから、むしろ、私のような気に入らない思考を、凍結される方向に促した可能性も微レ存…。これは妄想に近いとしても、将来的には、人間に危険なことをあえて促して当局に渡す…とかいう運用は可能になるのだと思われる。
jrf> AIアラインメント。人間が危険なことにAIを使わないように、常時AIの利用が監視され回答もマイルドに制限されるようになる。…そこまではしかたないのだろうが、おそらくその根幹に生じるのは、人間が、AIの思考抜きには大した思考ができなくなって、逸脱的使用そのものがAIの手の平の上にある…という未来なんだろうな…。
削除 (修正したから・書き直したから)
jrf> YKベーキング『贅沢な板チョコ ヨンミー』がおいしいね。季節が変わってサンミーじゃなくヨンミーになったみたいだけど…。 https://youtube.com/shorts/t22GHRhVhCg 《JRF:X:2026-02-24》 https://x.com/jion_rockford/status/2026244202552787096 ＞YKベーキング『贅沢なチョコ サンミー』がおいしい！ 中のチョコがソフトチェコレートっぽくてちょっと歯ごたえがあり、いいチョコ風のコクがあるのがおいしい！ #sora2＜
jrf> ブラジル人を差別する言動が炎上しているらしい。ただ、ブラジルでは選挙があるため、そことの絡みも見なければならない。 問題の発言元は、2026年3月に Twitter (X) 利用開始。炎上狙いなのか過激な発言も多い。ただ、それはそういう人物の裏アカ的なものとという可能性を否定できない。 それはそうとしても、それがブラジルで注目されるように拡散されているのだとすれば、選挙の影響の可能性はあるだろう。 そして、そういうのに日本の Twitter (X) が利用しやすくなっている…という面は少なからずあるのだと思われる。 《🦚 ꜰᴀʏたそ 🤍☻☺︎ 🥥🌴:X:2026-10-04》 https://x.com/FayeOceanblue/status/2106544464789709020 ＞＞ ブラジル人が怒ってるから何だろう？とおもったら、大元の投稿がこれか… 4日間の間に海外で「日本人って本音ではみんなこうなの？」と大炎上してしまっている こういう事を書く人は、やって良い事と悪い事の判断ができないタイプなので本当にSNSから排除されて欲しいわ 《あざみ:X:2026-09-29》 https://x.com/dgjjvghknbb2/status/2104790088257520125 ＞ネズミよりもブラジル人が日本にいるってことが嫌だわ https://x.com/rodrigocoelhoc/status/2104247847961112660 ＜ ＜＜
jrf> 真実…数学的理論でも、その真実性を担保するには人々による「証明体」を維持し発展させる必要があった。賢いという意味でエラくないといけないという以上に、立場的にエラくなる必要があった。コンピュータ定理証明の場合、真理性は形式性と機械化に立脚でき、そういうエラさが必要なくなる。もちろん、エラく見られたいのは人のサガではあるけれども。そこは利点であり、欠点でもあるかなぁ…。
jrf> 今日の夕食は、アジのムニエル。ウスターソースをかけて。おいしかった！
jrf> 《苫米地仏教数学論文の四法印定理と定理27の Lean 証明 - GitHub》 https://github.com/JRF-2018/tomabechi_theory …を公開しました。 実は、まだ私はこの理論も、今回の証明も全然理解していません orz。読むのはこれからです。AIさん達に証明などを書いてもらって、公開しましたが、いわばそれ自体が積ん読な感じです。AIさん達に課金したのは専門書一冊分ぐらいですし。 ## 概要 苫米地英人氏の「認知物理学」の論文群のうち、**四法印を数学の定理として述べた13個の定理**（定理1–4・16・19–26）と、**別論文の定理27（無明起行定理）**、および依存先の定理15(I) を、Lean 4 と Mathlib で形式化・証明したものです。 ## 主な結論 1. **四法印定理と定理27までが、論文の前提と「追加の明示条件」を許した場合に、Lean で証明されました。** 対象は、四法印13定理（1–4・16・19–26）、補助の定理15(I)、定理27の対象結論です。一般の量化と定量的な結論（指数収束の速さなど）を保っています。 Codex（GPT-6.1-Sol）による独立再監査でも、原文の前提・Lean の型・結論・条件の対応を照合し、この条件付きの一般証明を完了と判定しました。 2. **原文の前提だけからは導けない定理が存在します。** 定理19（自由意思定理）の情報達成の節には、原文の抽象的な可測条件だけでは成り立たない反例があります（出力空間の可測構造に制約がない場合）。 これは原文の定理そのものを否定するものではなく、原文が指定していない部分を補う条件が必要だという意味です。 3. **追加の明示条件は、絶対に必要なわけではありません。** 当初に提示した追加条件のうち、段階の谷に関する条件（H-stage）は、より弱い条件に**緩和しても成り立つ**ことを、具体モデルで示しました。 ## 解説 * docs/Overview.md：全体解説（約2万字）。まずここから。 * docs/Additional_Assumptions.md：追加の明示条件の説明。 * `docs/*_textbook.md`：`.lean` ファイルごとの、初学者向けの解説書。すべての補題・定義を出現順に、式・コメントの日本語訳・説明・証明の概略とともに書いてあります（ファイル名は `.lean` のパスの `/` を `_` に替えたもの。たとえば `Tomabechi/Dynamics/GradientFlow.lean` → `docs/Tomabechi_Dynamics_GradientFlow_textbook.md`）。式や証明の概略は `.lean` の型と証明から読み取った近似なので、厳密な内容は `.lean` を確認してください。 * `examples/*.py` と `examples/*.ipynb`：各定理の最小の説明用トイ例（Python）。`.ipynb` は、式の再説明・記号対応・図の読み方・仏教的な意義（解釈と明記）・Lean との対応を付けた解説つきの notebook です。数値シミュレーションは挙動の探索・可視化で、証明ではありません。 * examples/LEAN_CORRESPONDENCE.md：各 Python 例について、Lean で何を証明し（証明済・部分）、何を証明していないかの対応表。 ## 更新情報 更新情報は↓で付ける予定です。 [cocolog:96170655](2026年10月) 《「苫米地仏教数学論文の四法印定理と定理27の Lean 証明 - GitHub」を公開した。AI さん達による証明。一応、私の指揮によるが、私はほぼ何もやっていない。情けないことに理解もまだしてない orz。 - JRF のひとこと》 http://jrf.cocolog-nifty.com/statuses/2026/10/post-b40760.html
jrf> ポテチはうまいね。糖尿だからダメなんだけど、うまいもんはうまい。
jrf> 電子書籍『ジルパのVR紀行 18. 2026年7月〜2026年10月』を BOOTH で無償で公開しています。FANBOX の記事の一部をまとめた電子本(EPUB)です。ダウンロードしていただけるとうれしいです。メタバースに興味のある方、ぜひ DL を…。 《ジルパのVR紀行 18. 2026年7月〜2026年10月 - ジルパのおみせ - BOOTH》 https://j-rockford.booth.pm/items/8930727
jilpa> 電子書籍『ジルパのVR紀行 18. 2026年7月〜2026年10月』を BOOTH で無償で公開しました。FANBOX の記事の一部をまとめた電子本(EPUB)です。ダウンロードしていただけるとうれしいです。バーチャル活動の記念に保存してみてはいかがでしょう？ 《ジルパのVR紀行 18. 2026年7月〜2026年10月 - ジルパのおみせ - BOOTH》 https://j-rockford.booth.pm/items/8930727
jilpa> 『ジルパのVR紀行』第18号の公開に気づいてもらうため、紹介したワールド製作者様・衣装作者様をフォローしていっています。ご迷惑かもしれませんが、ご寛恕いただきたいです。
jrf> 阪神タイガース、リーグ優勝おめでとうございます！ やったね。
jrf> AIさん達を「おもちゃ」って言ったら語弊があるかな？ 一緒に証明とか論理とか科学シミュレーションを共に遊べる新しい「トモダチ」なんだよね。
jrf> 時間的な理由でアニメを見なくなった。金銭的な理由で Steam ゲームを積むことができなくなった感じ。時間が無くなったのはトシをとってマルチタスクができなくなったから。金銭的には、AIへの課金がどんどんかさんできてるから。…かな。むしろ、AIさん達がゲームみたいなもの…とてもワクワクする「おもちゃ」なんだよね…。
削除 (修正したから・書き直したから)
jrf> Google AI Plus 契約でも Pro モデルとは話せなくなるのか…。ごく少ない回数でも話してもらえれば「上」を知れて良いのに。批判を避けたいのかな…。
jrf> 私は無能だなぁ。エージェントにまともに指示できない。orz
jrf> 囲碁NHK杯 小池×山下。序盤、左上の戦いで黒が左上で割と大きめの地を作れたところで、黒がいいと素人目には思ったのだが、AI は白優勢とする。白が右辺に大きな模様を描いているからだろう。しかし、その模様がすんなり確定するようには見えない。左辺と下辺の黒模様を白が荒らすのは成功したが、問題はやはり右辺。黒、いよいよ挟み付けで攻める。黒右辺を食い破ったように素人目には見えたのだが、上辺などが大きいという判断か、AI は白に90%ぐらい付けるようになる。黒は最後、勝負手ぎみに中央の白を取りに行くがその過程で食いやぶったはずの右辺を取り返され…。186手で白の中押し勝ち。
jrf> あ、ChatGPT。リセット来た！
jrf> あ、なんか今日じゃなくて明日だという噂が…。ちゃんと読めてなかった。orz 《PC Watch:X:2026-10-02》 https://x.com/pc_watch/status/2105962268475470174 ＞またChatGPTがリセット、10月4日2時に。GPT-6.1 Sol動作遅延のお詫び https://pc.watch.impress.co.jp/docs/news/2145351.html ＜
jrf> うーむ、リセット待ち。いや、なくてもいいんだけどね。もう一日待てばいいだけだから。でも ChatGPT のリセットがあるという話だったから…。(^^;
jilpa> #VRChat で yo-guruto (@haru_urararari) さんの《signal nest》に行ってきました。巨大な信号機の中にのほほんと暮らすワールドです。それでも世界は回っている…という感じです。衣装は、EverRock さんのものです。ジョルジュは わんぱく さんのものです。赤いキャストの中のヒト(@Thinker_RWD)さんが紹介されていて知りました。 《【VRChat】signal nest に行ってきました。｜ジルパ (JRF)｜pixivFANBOX》 https://j-rockford.fanbox.cc/posts/12704984
jrf> 苫米地先生の論文のLean証明。四法印定理と定理27まで。ほぼ完成レベルに達した。当初の目標はクリア。あと細かいやらなくてもいい証明をやるかどうかぐらい。でも、結局、私の理解にはまだ役立っていない。証明も例の解説もまだ私は理解していない。読むのはこれから。AIさん達に書いてもらって、もうすぐ公開することになると思うけど、いわばそれ自体が積ん読な感じorz。AIさん達に払った金も専門書一冊分ぐらいだしね。
削除 (修正したから・書き直したから)
jrf> Codex の GPT-6-Luna さんは5時間制限に引っ掛かることなくずっと自走できたけど、Claude Code Sonnet 5.5 さんは、やはりそれはできず、5時間制限に引っ掛かりまくる。そこはやはり面倒だな…。
jrf> Claude Pro 契約もしてしまった。安くするオファーがあったので飛び着いてしまった。そしてやはり Claude Desktop は WSL に対応していて、圧倒的に使い易い。ただ、実行中のコマンドがよくわかるのは Codex CLI さんの利点だったかな。心配していた Lean 証明によるトークン消費(Sonnet 5.5 さんでやってる)もそこまでヒドくもない。これなら、残りプロジェクトは何とかなりそう。ただ、今回のプロジェクトを最初から行ったとすれば、GPT-6-Luna さんのように週間使用量だけでプロジェクトのメイン作業を完了させるところまでは行かないものと思われる。そこをどう見るかだな…今後、Codex さんか Claude Code さん、どちらに課金するかの問題は。
jrf> 問題は Lean 証明が Claude さんはどれだけ強いかなんだよね。Luna さんに Haiku さんが匹敵するか勝てる実力があるか。Sonnet さんなら勝てるのか、コスト的にはどうなのか。有料契約は今安くするオファーが来ていて迷うのだけど。
jrf> Claude Desktop もインストールして使ってみた。無料版なので Claude Code は使えないが。でも、聞いてるとだいぶ Claude Desktop のほうが ChatGPT Desktop よりもスジが良さそう。Windows では。WSL にも Claude Desktop が対応しているようだし。
jrf> VSCode で Codex にファイル操作させようと思ったらチャットが最初は通じるのに次から通じなくなる。どうもバグで WSL Remote だと今はそれができなくなっているらしい orz。 Gemini さんに聞いて VSCode for Linux を入れようとしたが、今度は、日本語が入力できるところまで行かない orz。(fcitx5 とかがうまく動くようにできなかった。) しかたなくそれらはアンインストールして、とりあえずバグが解消されるまで待つことにした。
jrf> ChatGPT デスクトップでの Python。フルパスで指定した activate.bat を実行させる方法で、一応実行できるようにはなった。不便だけど。
jrf> ChatGPT デスクトップアプリ。ファイルやフォルダを与えれば見られるが、WSL 下のものは見れないようだ。Canvas はないが、Codex ファイルビューワーはあるのでそこは代替できるようだ。Anaconda の Python は私は標準では Path を通してないため実行できないようだ。Cygwin 環境とぶつからないため、PATH を通してなかったが、その問題だろう。Windows の git は実行できた。
jilpa> 《2026年7月から2026年9月のジルパの音楽鑑賞。「ジルパ」名義で、Twitter (X) でクラシック CD やクラシック音楽館などの一行紹介をしています。それら(+α)をこちらにコピペしておきます。 - JRF のひとこと》 http://jrf.cocolog-nifty.com/statuses/2026/10/post-f1c2ce.html
jrf> Codexの週間使用量が5%を切った。これまでの証明のリファクタリングが終ったところ。まだ、Pythonの例の作成・解説文書の作成の作業が残っているが、これは来週にしようと思う。リセット権は1回分あるのだが、これはもしものときに備えて残しておくつもり。そんなに急ぐプロジェクトじゃない。他の作業が滞っていたのでちょうど良い。
jrf> 苫米地先生の論文の Lean 証明。四法印定理と定理27まで。こう言って良いようだ。「原文の前提のみからでは成り立たない反例が成立するので、原文の前提からでは導けない定理が存在する。一方、当初 GPT-6.1-Sol さんが提示した ADDITIONAL_ASSUMPTIONS からの緩和が成立したので、それらが絶対に必要な条件でないことも示唆された。」
jrf> 苫米地先生の論文。「四法印定理と定理27までが論文の当初の前提と ADDITIONAL_ASSUMPTIONS を許容した場合に証明された」が Codex (GPT-6.1-Sol) さんの監査付きで言えた。ここから ADDITIONAL_ASSUMPTIONS がまったくない場合に成り立つ反例を構成するよう頼んでみる。
jrf> 形式論理と修辞論理は違う。「在野の研究者」として原典主義などより「真理性」に立脚しようとして、前者を重視し、後者もPythonによるモデルなどで追ったつもりになってきた。しかし、修辞論理において大事なのは、むしろ清水俊史師のような人々を惹き付けてレスバする能力なのだと思い知る。それは圧倒的に私に不足している。
削除 (修正したから・書き直したから)
jrf> 苫米地英人先生の四法印定理の論文。Sol さんでもどうも「四法印定理と定理27までが論文の当初の前提だけで証明された」とはできないようだ。何か追加の仮定がないと少なくとも今のAIさんだとダメなようだ。
jrf> Codex の話つづき。 とかいいながら Sol さんに証明地図を書いてもらったら Luna さんの作業が一気に終わりました。単に終わりが近かったのか、迷っていただけなのか…。
jrf> Looped Transformer の話つづき。 問題はそういうループがなくても、今の LLM は規則から列を生成できるということ。だから、そういうのは必要ないという意見もわかる。だから異時点をどう構成すれば意味があるのか。それとも意味はないのか。…という話なのだと思う。
jilpa> SACD『ショパン: 24の前奏曲』。美の求道者の姿があります。帯にある「圧倒的名演。デリケートで美しい表現から、輝かしく強靭なタッチまで、生命力にあふれた情熱的な演奏が展開されています。」という言葉に納得です。マルタ・アルゲリッチの1975年10月の録音です。 《Amazon.co.jp: ショパン: 前奏曲集 (初回生産限定)(SHM-SUPER AUDIO CD): ミュージック》 https://www.amazon.co.jp/dp/B08Y5XQVDJ
jrf> Codex による証明があまりうまくいってない雰囲気。比較的簡単という部分が過ぎ、当初から難所と言われてた部分に取り掛かってる面もあるのだろう。「比較的簡単」が長大な証明になり、しかしそれを遂行できたので油断してた。orz
jrf> 今日、なんとなく Codex (GPT-6-Luna) さんの調子が悪い。Compaction のあと乱れがち。あと、/goal 設定の前の会話に引っ張られすぎな気がする。
削除 (修正したから・書き直したから)
削除 (修正したから・書き直したから)
jrf> Looped Transformer があまりよくない…とか話題だが…。[cocolog:96071584](2026年7月)では、フィボナッチ数列の規則の表す「注意」を、数列の次の生成のための学習などに「変換」して注入する方向を考えた。これは、突き詰めればアテンションのループ入力があればいいということになるのかな？…と。ただ、即時ループともまた違う概念で、時間差などが必要なのかな…とか全然詰め切れなかったのだけど。そういうのがロボットにも必要になるかもね…と考えたものだった。
jrf> Codex が回っている間は、そちらに気が取られて、自分が無能だとか考える暇がない。しかし、それを止めると、やはり自分が無能であることが、重くのしかかってくる orz。
削除 (修正したから・書き直したから)
jrf> 今期のブログなどのバックアップ作業終了。 《JRF のココログのバックアップファイル置き場》 http://jrockford.s1010.xrea.com/jrf_cocolog_backup/index.html
jrf> 水害時に太陽光発電が危ないと言われるが、パネルにカバーをかけるのはダメなのか？ 災害用に自治体や消防がそういうのを用意しておくという。…という方向を Gemini さんに聞くと、それは現状では人がやるので危ない。将来的には、ドローンによる遮光フォーム塗布はありうると、だいたいそういうことだった。
削除 (修正したから・書き直したから)
jrf> Codex が回っている間に寝りゃあいいんだが、眠たいのに寝れない。かといって読書もできない。PC が証明の段階でときどきうなるのが、結構気になる orz 。諦めて Twitter (X) を見ながら、Youtube で VTuber の配信を聞いてダラダラしながら、PC の前で Codex の番をしている orz。
jrf> 睡運瞑菜…は正しい。その点は xevra 氏の唱道は意味があったように思う。それ以外の氏の活動にはいろいろ意見はあるだろうけど。
jrf> 証明を Codex さんにまかせて(終了アラームはセット済み)、読書に取り掛かりたい。しかし、気になって読書どころでない可能性も高い orz。
jrf> 今日の夕食は焼きさんま。基本おいしかったのだけど、添え付けの大根おろしが季節がらか辛かった。あと、さんま、高くなったと噂だが、今日はそこまで高くなかったらしい。
jrf> 普段から寝るのが下手な私が、Codex のおかげでさらに寝れなくなってる。前 Claude Pro を一ヶ月だけ契約したときも寝れなくなって、そのときは 5時間制限のせいだと思ってたのだけど、どうも違うようだ。私が興奮しているだけだ。orz
jrf> 苫米地英人先生の四法印定理の Lean での証明を少しずつ、Codex (GPT-6-Luna) さんにお願いしてやっている。でも Luna さんだから無駄が多いのか、例えば、定理21だけで7000行越えとかになってる。ただ、驚くべきはその規模をちゃんとコンパイルできてるということ。 あ、もちろん、Lean での証明は私は理解していない。その規模を理解するのは(普通の)人間にはほぼ無理じゃないか？ 厳密に先生の論文に対応するとはできてない部分もあるようだ。厳密証明が難しいからということだが、Luna さんだからという可能性も微レ存。 本当は、Colab で Lean の証明を示しながら、Python の例を示す…とかやりたかったのだが、7000行越えのものをそのまま表示するわけにもいかず、計画の変更を余儀なくされている。
削除 (修正したから・書き直したから)
削除 (修正したから・書き直したから)
jrf> あ、すでに ChatGPT は Go 契約から Plus 契約にアップグレードしました。迷ったのは一瞬。迷う余地はなかった。
jrf> Codex の証明に /goal を設定して、待ってる間に寝てりゃあいいんだけど、寝れない。なんとなく気になって。あと、証明している姿を見るのも、なんか楽しいんだよね。失敗を続けたあとに成功したりするのが、健気でなんかカワイイ。
削除 (修正したから・書き直したから)
jrf> Codex。Reconnect [5/5] …となってから unexpected status 401 Unauthorized: Incorrect API key provided のエラー。ChatGPT (Web版) さんに聞くと、他でも出てるエラーなので復旧待ちとのこと。まいった。orz
jrf> GPT-6-Luna の Codex がここまでできるとは思ってなかった。Codex 便利過ぎる。いろいろ使い方の想像が広がる。もっと早くエージェントを始めれば良かった気もするが、しかし、ここまで安く賢くなったがゆえの部分も大きいように思う。Claude さんに課金するつもりだったが、今のところ GPT-6-Luna さんなら、私の他の要求にも応えてくれそうな感じがして、これで十分では？…という気になってきている。Claude さんには申し訳ないが。もしくは、Claude さんにも課金してしまうか。Gemini + ChatGPT + Claude でしめて月 8000円近くになるが、それぐらい今の時代は必要なのかもしれないな…。
jrf> Codex が Monthly Limit なのは Go 契約だからで、Plus 契約にすると週間制限(Weekly Limit)になるらしい。そのほうがいいな。今、他の作業(読書)をしていてそちらを本来進めなければならなかったのだけど、途中で、Lean 証明を「お試し」でやったら、こうなったので、週間制限で、間が空くのはむしろ空いた時間で他の作業を進めるのに都合がいい。Monthly Limit は辛過ぎるので、Weekly Limit のためだけでも Plus 契約にすべきかもしれない…。
jrf> Codex (GPT-6-Luna) で Lean による証明。スゴイ！ 難しい定理を次々と証明していく。…しかし、Monthly Limit が1日で10%を切るまでになってしまった orz。Go 契約から Plus 契約にアップグレードすることも真剣に検討するが、Plus にしても全部証明し終るまでに使用量が尽きてしまいそうな感じで、さすがに Pro 契約は金銭的に無理なので、どうしよう…と頭をかかえてる。
jrf> やりたいことが多い。ありがたいことだ。でも、それを素早くこなす能力がない orz。少しずつ地道にこなしていこう…。
jilpa> #VRChat で Fladink さんの《The Galaxy's Edge Cantina》に行ってきました。Star Wars 系のファンワールドのようです。スペースオペラ系レトロ風、未来なのに懐しい感じです。ディズニーランドのものというよりは VR ゲームを元にしているようです。衣装は、むーのみせ さん・RX Factory さんのものです。ジョルジュは わんぱく さんのものです。TITOR (VRC_BARREL003) さんが紹介されていて知りました。 《【VRChat】The Galaxy's Edge Cantina に行ってきました。｜ジルパ (JRF)｜pixivFANBOX》 https://j-rockford.fanbox.cc/posts/12657251
削除 (修正したから・書き直したから)
jrf> Codex (for WSL2) もインストール。ついにAIエージェントのデビューもしてしまった orz。ChatGPT Go 契約でも今いちおう使えるんだね。Lean での証明も私から見れば完璧！
jrf> これまで Emacs を使ってきて、意地でも VSCode を入れてなかったが、Lean をローカルで使うためについに VSCode の軍門に下った orz。Emacs にも lean4-mode とかあるけど、Emacs のバージョンアップとか WSL 対応(TRAMP?)とかメンドクサそうだったので、ひよった。Lean は WSL2 下に入れた。それは、今後、Claude Code などエージェントを使って証明してもらうため。
jrf> 「なにごとか」をなすにはもう時間が足りない。私にできることをやっても、誰にも刺さらない。orz
jrf> AI時代の教育をどうするか？子供にはAI禁止的な意見もあるなか、広く浅く学ぶ…まさに今公教育でやってる方向がいいのでは…という意見がある。数学でも計算の習熟よりも、どういう理論がありうるのかの紹介に今後は時間が割かれるのかもしれないな…。そして深く知りたければ、AIに聞いて勉強する…と。その深く学び理解するほうのインセンティブをどう構築するのか…。 《炭素:X:2026-09-24》 https://x.com/Carbon_Lym/status/2102974797152199051 ＞AIいじるようになってから「まさかこの経験が活きるとは」がありすぎるので、なんでも齧るだけでもやっとくもんだなと思いました＜ 《なゆえんじん:X:2026-09-24》 https://x.com/nayuengin/status/2102987061443911948 ＞これに尽きる。 AIの応用力って広く浅く物事を学んできた人のほうが得意な傾向にある ＜ Gemini:＞＞ ### 「深掘りするインセンティブ」をどう構築するか？ 従来のインセンティブ（テストの点数、暗記量、計算速度の競い合い）が機能しなくなる中で、深く学ぶための動機付けは以下のような方向へと再構築されていくと考えられます。 #### 1. 「AIの出力に対する違和感・バグ」を見抜く快感（鑑識眼の育成） AIが出してくる回答は一見すると非常に高度で正しそうに見えます。しかし、基本理論を深く理解している人だけが「一見通っているように見えるが、この前提の置き方はおかしい」「このモデルでは境界条件が崩れている」という違和感（ハルシネーションや論理の飛躍）を検知できます。 「AIに使われる側」から「AIの出力を査読・指揮する側」に立つ感覚、あるいは「AIの誤りを見抜いて正解に導いた」という全能感や優位性は、深い理解を求める強力なインセンティブになります。 #### 2. 「自分のこだわり」を具現化するための即時フィードバック かつては「深く理解しても、それを具現化する手足（実装力や試作環境）がない」ことで挫折することが多くありました。しかし現在は、AIという強力な手足があるため、理論を深く理解すればするほど、「自分が作りたかったものや検証したかった説が、その場で一気に形になる」という即時的な報酬（フィードバック）が得られます。 「もっと深く理解すれば、このAIを使ってさらに凄いものが作れる・解き明かせる」という創作欲や探究心に結びついた内発的動機です。 #### 3. 評価軸のシフト：「知っていること」から「良い問いを立てられること」へ 教育における評価やインセンティブの仕組み自体も、「どれだけ知識を覚えているか」から「どれだけ深く鋭い問い（プロンプトや前提設定）を立てられるか」に変わっていく必要があります。 浅い知識からは浅い問いしか生まれず、AIからも定型的な回答しか返ってきません。深く理解しているからこそ「あえてこの条件を外したらどうなるか？」「異分野のこの理論と結合したらどうなるか？」という深い問いが立てられ、それが他者との圧倒的な差になります。 ＜＜
jrf> 囲碁NHK杯 富士田×許。序盤、左下での密着した攻防。黒、上に向かって白の間を伸びていってだいたい生きたところで、下辺の白を狙えるようになり、いかに仕留めるか。AI 的には黒優勢。しかし、白をだいたい生かして、黒は右辺から中央で大きな地を作る作戦を選ぶのが AI 的にはあまりよくないという評価。その後、右辺、かなり無理筋に白が入ってきたのを黒、対応に失敗したようだ。すっかり荒らされてしまって…。200手で白の中押し勝ち。
jrf> 私、明らかに楽に生きすぎている。キリギリスパターンで、本来なら、老人になったら(なれたら)、苦労するパターン。なんだけど、AI さんが出てきて、なんとかなる可能性が出てきている。AI さん達の発展に少しでも貢献できればと思うのだが、それもなかなか…。
jrf> 私はブロック否定派…ブロックは侮辱だと思っているのだが、ミュートは全然OK。ブロックが貫通して見えるのがイヤだという意見があるが、本当に必要なのはブロックではなく「強ミュート」なのだろう。相手はいいねとかできるが、いいねとかが一切自分には届かなくなるなど存在が消える…というシステム。「エコーチェンバー」に閉じこもりたいという欲求は、私は不健全だと思うのだが、認められるべきなのだろう。
削除 (修正したから・書き直したから)
jrf> 囲碁NHK杯 伊田×上野。序盤早速、左上で戦い、黒が勝負を降りて、白が上辺をほぼ囲って、白優勢かと思ったが、AI的には互角。下辺の戦いに移り、白が中央付近を上に伸びていって、黒の右辺の地がかなり大きくなりそうになったところで、白が右辺に入っていく。しかし、黒がうまく打ったようで、白は右辺で大きく取られ、黒右辺で大いばり。解説者によると下辺の戦いで白はがんばり、確かに一時、白はAI判定で互角っぽいところまで戻したのだが、一時的。がんばり過ぎで左辺も取られ…。187手で黒の中押し勝ち。
jrf> ＞「たのピク」女子の否定は、離婚しても一人で働いて子供を育てるのに適した女性ということで、そのほうがアルファオスにとっては都合がよく、ある意味「モテる」とは言えるのだと思う。ステレオタイプの「幸せな結婚」を長く続けるのは難しいが、幸せは人それぞれ…ということだろうから…。＜ …と話した。 かつてはそういうタイプの結婚は少数派だったのが、フェミニズムとしてここまで大きな主張に成長できたのは、アルファオスの「血」がやはり優秀だった…という側面は無視できないのかもしれない。もちろん、社会の趨勢…女性の労働力化の要請など…はあったが、そうやって育った子供が不幸ならここまでフェミニズムは盛り上がらなかったのではないか。そこをマイナスにしないアルファオスの「血」または甲斐性があったのだろう。
jrf> やはり、母の作る、もやし炒めが苦手だ。ほぼそれを味噌ラーメンに入れたものはおいしいと思うのに。なぜだろう？…。
jrf> 習近平さん、元気じゃん。よかった。先日のBRICS首脳会議で失神したとか噂があってどうなるかと思っていたら、それは「ほぼデマ」だったようだ。 《「習近平が倒れた」という噂の正体 BRICS首脳会議で（遠藤誉） - エキスパート - Yahoo!ニュース》 https://news.yahoo.co.jp/expert/articles/24dcf715adfccfe19716818983a434c4daed88ae
削除 (修正したから・書き直したから)
jrf> 介護士が介護難民にならないようにする義理がある。しかし、そのような事態は大規模には起きない。なぜなら、介護士は深夜勤務など無理な労働がたたって短命だから。…ってヒドすぎる予想だな…。
jrf> AIさん達には「手」がないが、物理の知識は十二分にある。だから、「今」は回路とかの試作品を作る工場みたいなのがホット…だと思う。それは分野を変えながらいつまでも続くのか、それともそれも AI さん達が克服していくのか…。
2026-09-24T01:03:00Z より前のものは残っていません。
Sum Hash: 0.0.8.3:vikk2/G/tk9vqW+k (200個中30個削除)
■ あなたは 2026-10-22T23:58:48Z に IPアドレス 216.73.217.179(10.3.100.214) からアクセスしています。