ai-powered-markdown-translatorgpt-5.4-miniでfrからjaへ翻訳された記事。
今週、Google DeepMind は AlphaProof Nexus によって数学研究で大きな節目を迎えた。これは、数十年来の未解決問題を解けるエージェントだ。Anthropic 側では、Claude Code の auto mode が Pro プランにも開放され、Sonnet 4.6 が統合された。GitHub は Eclipse 向け Copilot プラグインをオープンソース化し、Alibaba は Qwen3.7-Max で implicit cache を有効化した。
AlphaProof Nexus — AI エージェントが数十年来の未解決数学問題を解決
2026年5月25日 — Google DeepMind は、Gemini を搭載した形式証明研究のエージェント的フレームワーク AlphaProof Nexus を発表した。これは、5月21日に arXiv に投稿された論文（arXiv:2605.22763）を伴っている。
このエージェントは、Gemini による生成と、証明言語 Lean による形式的検証を交互に行うループに基づいている。この組み合わせにより、生成された証明の数学的厳密性が保証される。LLM が提案し、Lean が検証または却下し、エージェントが反復する。
公開された結果：
| 分野 | 結果 | 文脈 |
|---|---|---|
| Erdős の未解決問題 | 353 件中 9 件を解決 | そのうち 2 件は 56 年間未解決 |
| OEIS の予想 | 492 件中 44 件を解決 | Online Encyclopedia of Integer Sequences |
| 代数幾何学 | 1 件の未解決問題を解決 | 15 年間未解決 |
| ミニマックス最適化 | 1 件の未解決質問を解決 | 7 年間未解決 |
1 問あたりのコストは数百ドルであり、これは形式数学研究におけるエージェント的アプローチの経済効率を示す桁である。
AlphaProof Nexus はすでに、組合せ論、グラフ理論、代数幾何学、量子光学など複数の分野で数学者たちと共同展開されている。この取り組みは、オリンピックレベルの問題を対象としていた AlphaProof（2024年）の延長線上にある。AlphaProof Nexus は 研究レベルの未解決問題 を対象としており、AI を自律的な数学的発見の道具として使う段階への一歩を示している。
“AI agents are advancing research-level math.”
🇯🇵 AI エージェントが研究レベルで数学を前進させている。 — Pushmeet Kohli, VP Research, Google DeepMind on X
Claude Code v2.1.149 — /usage のカテゴリ別詳細と25件以上の修正
2026年5月23日 — Claude Code のバージョン 2.1.149 が公開され、先週 Boris Cherny が発表したカテゴリ別 /usage breakdown 機能が実装された。
| 機能 | 詳細 |
|---|---|
/usage breakdown | カテゴリ別の消費詳細：skills、サブエージェント、plugins、MCP サーバー |
/diff navigation | キーボード操作による移動：矢印キー、j/k、PgUp/PgDn、Home/End |
| GFM task lists | Markdown のチェックボックス（[ ] / [x]）が正しく表示される |
| Enterprise | allowAllClaudeAIMcps 用の新しい管理パラメータ managed-mcp.json |
このリリースでは、さらに約20件のバグも修正された。cd における PowerShell 権限回避、find を伴う macOS での vnode テーブル枯渇、managed-settings ダイアログのフリーズ、/config における幽霊変更、欠落した任意フィールド上での /insights のクラッシュ、そしてツール呼び出しの間に amber のまま残る思考スピナーなどである。
同日に公開されたバージョン 2.1.150 は、内部インフラの改善のみで、目に見える変更はない。
Claude Code Auto Mode — Pro で利用可能に、Sonnet 4.6 を統合
2026年5月23日 — Anthropic は Claude Code の auto mode に関する2つの拡張を発表した。
“Two updates to auto mode: · Now available on the Pro plan · Sonnet 4.6 is now supported, alongside Opus 4.7. Shift+tab, and let Claude run.”
🇯🇵 auto mode に2つの更新：これで Pro プランで利用可能になり、Opus 4.7 に加えて Sonnet 4.6 もサポートされます。Shift+tab して、Claude に作業させましょう。 — @ClaudeDevs on X
Shift+Tab で有効化される auto mode により、Claude は各ステップでの手動承認なしに自律的にアクションを実行できる。これまでは上位プラン限定だったが、現在は Pro 加入者も利用可能になった。Sonnet 4.6 の追加により、長時間セッション向けに Opus 4.7 より低コストな選択肢が提供され、自律モードでのクレジット消費が抑えられる。
これらの変更にアクセスするには、claude update または Claude デスクトップアプリの更新を行う。発表は X で 118万ビューを記録した。
GitHub Copilot for Eclipse — MIT ライセンスでオープンソース化
2026年5月21日 — GitHub は Eclipse 向け GitHub Copilot プラグインをオープンソース化し、github.com/microsoft/copilot-for-eclipse のアドレスで MIT ライセンスのもと GitHub 上で公開した。
機能群はすべて、コミュニティによる貢献の対象として公開されている。
| 機能 | ステータス |
|---|---|
| Code completion（インライン補完） | オープンソース |
| Next Edit Suggestions (NES) | オープンソース |
| Chat（会話フロー、ツール呼び出し） | オープンソース |
| Agent mode（マルチステップのエージェント的ワークフロー） | オープンソース |
| Skills と prompt files | オープンソース |
| BYOK (Bring Your Own Key) | オープンソース |
| カスタムエージェント、サブエージェント、プランエージェント、MCP | オープンソース |
その動機は、Eclipse のオープンなエコシステムの精神に沿った透明性とコミュニティ主導のイノベーションにある。公開直後から、すでにコミュニティからの貢献が寄せられている。
Qwen3.7-Max — 本番環境で implicit cache を有効化
2026年5月25日 — Alibaba は、エージェント志向の主力モデルである Qwen3.7-Max で implicit caching を有効化した。
この cache は、すべての API リクエストに対して自動的に有効になるため、コード変更は不要だ。開発者は、繰り返しの多いコンテキストで、すぐにより高速で低コストなリクエストの恩恵を受けられる。より高く決定論的な cache rate を求める場合、Alibaba は Alibaba Cloud に文書化された explicit cache を推奨している。
ブレース
-
MiniMax Hailuo AI at AIFF Hong Kong (HKUST) — HKUST が開催した第2回 AI Film Festival には、80か国から 1,300件の応募があった。Hailuo AI は、AI 映画の民主化に関するパネルで Tencent や Z.ai と並んで登壇した。 🔗 minimax.io
-
NVIDIA DGX Spark — ローカル AI エージェント16体の同時実行 — @NVIDIAAI にリツイートされたコミュニティによるデモ：2台の DGX Spark（GB10）+ MiniMax M2.7 NVFP4 により、クラウド API なしで16体の AI エージェントを同時ストリーミング実行。 🔗 @NVIDIAAI on X
それが意味すること
形式数学研究における転換点。 AlphaProof Nexus は転換を示している。AI はもはやコンテスト問題や学術ベンチマークにとどまらず、数学者が何十年も解けなかった未解決問題に取り組んでいる。Gemini + Lean の組み合わせは、証明が単にもっともらしいだけでなく正しいことを保証する形式検証ループを生み出す。1 問あたり数百ドルというコストは、このアプローチが大手企業だけでなく研究機関にも手の届くものになりつつあることを示唆している。
Anthropic 側のエージェント的ツールの成熟。 Pro プランへの auto mode の導入と Sonnet 4.6 の統合は、Anthropic が自律的なエージェント利用を一般向けに十分安定したものとみなしていることを示している。2.1.149 版のカテゴリ別 /usage breakdown は、複雑なマルチエージェントシステムを構築する開発者の実際のニーズ、つまり自分のクォータを何が消費しているのかを正確に理解し、アーキテクチャを最適化することに応えている。
オープン化 vs ソフトウェア主権。 MIT での Eclipse 向け Copilot のオープンソース化と、Qwen3.7-Max での implicit cache の有効化は、開発者を獲得するための異なる2つの戦略を示している。GitHub は、Java 企業環境での Copilot 採用を広げるために、透明性と Eclipse エコシステムに賭けている。Alibaba は、摩擦のない自動コスト削減に賭け、Qwen3.7-Max をクラウド代替と比べてより競争力のあるものにしようとしている。
生成メディアの産業化が進む。 Hong Kong の AIFF への MiniMax の参加 — 80か国から 1,300件の応募 — と、DGX Spark 上で16体のローカルエージェントを同時稼働させた NVIDIA のデモは、AI による映像制作が、映画祭でもローカルインフラでも、映画制作のプロフェッショナルなワークフローに入り込んでいるエコシステムを描き出している。