LLMを使って、フェルマーの最終定理が1300万行で形式化され、ナビエ-ストークス問題は外力ありの場合、有限時間で解が発散する形で解かれたようです。
ホッジ予想とBSD予想の解決も近いとか。
AGI/ASIに向かって世界が大きく変わりつつあることを実感しつつ、世界に100人しか理解できない理論が1300万行のコードになっても凡人には世の中何一つ変わらないなと😅
これからは証明は(命題の価値が認められた時に多額の費用をかけて)機械がすることで、数学者は数理の美しい構造の発見に専念するのかもしれません。
一方でこれは数学者の生き残りのために、既得権益と権威の強化を強く進める方向に働き、数学界はますます、ペレルマンさんが関わりたくないと思うコミュニティになるのかもしれません。
この数日、AlphaGo以来の喪失感を味わっています。
(AIが働いて人はBIで楽しく暮らす社会に早くなりますように🤪)
遅ればせながら、Antigravityで初めてAIエージェントを試しました。
便利ですね。
パーサをちょっと書いてもらって「こりゃすごい！」と思ったのですが、すぐクォータが切れて2週間待てと…
流石にこれでは使い物にならないので、VSCodeの拡張Clineを導入しました。
サブスクは好きじゃないので、従量課金にすべくGemini API。
(余談ですが、最近までGeminiで満足していたのですが、あっちこっちあれがいいこれがいいという話を聞くとGeminiもひとつかな？という気分になったので、AIの評価というのは難しいものですね)
で、エージェントで何をしようかなと思ったのですが、やっぱりこれを機会に数学かと。
数学はついに、AIというツルハシで挑める金鉱という時代になりました。
なので、Leanを1行も書いたことがないLean使いになろうかと。
難しい現代数学よりオイラー辺りのほうが好きなのでその辺から遊ぼうかな。
追記。
n^2が偶数ならnも偶数の証明に$0.5かかりました。(無料枠も使ったから実際にはもっと？)
そして…できたコードがよくわからない🤪
最近、Geminiがお気に入りです。実際、無課金勢には今一番性能がいい気がします。
で、しばらく使っていたSafariをやめてChromeに戻りました。Gemini in Chromeのためです。
見ているサイトの話ができるっていいですよね。AIアプリにURL貼っても読めないことが多いし。
ところが、Gemini in ChromeはグローバルにCntl-Gをフックしてショートカットにします。
Cntrl-Gってエディタの必須ショートカットですよ？？何してくれるん？です。
Chromeの設定の「AIイノベーション」から「Gemini in Chrome」の設定を開くことができます。
そこにショートカットの設定があるので、他のキーかショートカットなしにすればOKです。
WWDC 2026で一番気になったのがAFM 3 Core Advancedでした。
どうも、12GB以上のDRAMを持つ端末限定で、20B級VLMが動くようです。
20B級は知識としても相当です。これはすごい！
ウェイトをDRAMに全部置かずに決めたMoE分SSDから読むとか。
でも、なんかもやもやするんですよねぇ。
少なくともApple純正機能としては、そのAFMを使うかをユーザーに選ばせる気はなさそうです。
必要に応じて適したモデルを使う。
ということは、Core Advanced未対応の端末の場合、処理はPCC(Private Cloud Compute)が処理することになりそう。
Cloudなので当然、レイテンシーとか悪くなり、プライバシーも若干心配になります。
でも応答が稚拙になることはなさそう。
もしかしたらPCCではなくCoreにフォールバックするかもしれなくてその場合、応答は稚拙になるはずですが。
もしCoreにフォールバックしなかったら、なんかレイテンシーを忘れると、Core Advancedって、クラウド代大変だから12GB DRAM端末は自分で計算してくれっていうせこいサービスに思えませんか？
もしかしたら、Core Advanced未対応端末を使うことがApple Intelligence勝ち組かもしれません🤪
Swiftでガチガチのチューニングに挑戦して挫折しました。
今更C++も大変だし、Rustもアイデアは素敵と思ってもコーディングは何かしんどいという感じ。
諦めかけていたところ、Zigを知りました。
Rust is a better C++, Zig is a better C.
だそうで、その通りの言語仕様です。
メモリモデルがRustのように目新しくないので、文法さえ知れば普通に書けます。
まだ、バージョン1に到達していなくて破壊的な改良が続いているのでプロダクションに使うのは難しいと思いますが、正式版が出たら一定の層に流行ると思います。
Python/Swift/Zigの3つの言語がそれなりに使えたら大体満足できそう。
Python, Swiftの代替候補は色々ありますが、3つ目のC/C++/Rust層がつらかったんだよねぇ。
「俺の最強言語」という厨二病を持ちながら3つの言語で頑張ればいい😁
というわけで、Zigが無事正式リリースを迎えることを心から願います。
できれば貢献したいな。何かツール作ろうかな？
今年1月のProject DIGITSの発表から10ヶ月弱、ようやくDGX Sparkが出荷され始めました。
LLMについて色々調べて、特にToken Generationはメモリ帯域律速だということもわかって、DGX Spark、1PFLOPSの割にきついんじゃないかという気がしていました。
ベンチマーク結果は、M3 Maxと同じぐらいのようです。メモリ帯域(Spark 273GB/s, M3 Max 400GB/s)を考えると善戦。
(というか、M3 Maxチューニング足りてないのかも)
さて、値段ですが、日本では代理店経由で価格未公開が多いですが、公開しているところを参考にすると、税込70万円かそれ以上。
同等のスペックをMac Studioでカスタマイズすると、
で、税込733,800円。
AppleのSSDは高速ですが、Apple税が入っているので？節約コースを考えると、
583,800円＋40,000円=623,800円。DGX Sparkより安いです。
CUDAに慣れていてLLMをゴリゴリしたい人にはDGX Sparkはいいかもしれませんが、その辺りはお任せ、大きなLLMを動かして使いたいだけという人には、Mac Studioがお値打ちなようです。
一番に最初に、LLMにはMacがいいと言った人の先見の名に感心します。
当時、私も、LLMと言えばNVIDIA GPU必須やろ、さすがにMacがいいは言い過ぎと思いました。
AI PC/Copilot+ PCも基本UMAですが、Macほどその自由度が高くないようです。
NPUがメモリをフルにアクセスできなかったり帯域が絞られていたり。
というわけで、DGX Spark欲しい熱が冷めて、Mac Studioいいなぁと思いながらIntel iMacでブログを書いている今日この頃です。
struct InlineArray<let count : Int, Element> where Element : ~Copyable
InlineArrayのシグニチャを見て、「え？Elementはコピーできないの？なんのこっちゃ」と思ったのですが、今時のLLMに聞くとこれは「コピーできてもできなくてもいい」という意味らしいです。
そして、whereでElementがコピーできないという制約は書けないらしいです。
狂っている。控えめに言って狂っている。
この瞬間、Swiftの嫌なところがどっと湧いてきました。
classとstructって何？最初は参照型か値型かでメンタルモデルも作りやすかったです。しかし今では特に大きなデータの場合、結局どっちで作るのがいいか、ほぼどうでもいいのに決定しなければいけない無駄な意思決定を要求されます。
DispatchQueueかasync/awaitか。async/awaitのほうが効率良さそうなのはわかります。しかし移行するのにHaskellのモナドぐらい敷居があります。一つasyncで書くと、利用しているメソッド群を雪崩式にどどどっと書き直さないといけない。過去のリソースを使わない新規プロジェクトならいいですが、そうじゃない場合、結局両方書けっていうこと？
SwiftUIって結局、ロジックとUIの分離が難しくなってない？MVCかMVVMかTCA？もうええって。
ずっと、Swiftラブだったのに。愛はいつか冷めるもんですね。
ああ美しい言語と出会いたい。
