2026.07.22 —— 今日 10 則
TODAY'S THREAD 今天一條線是 AI 把能力邊界往外推——從 LLM 產出 Jacobian 猜想的反例、到一整隊 Claude 併發寫出能編譯 Linux 的 C 編譯器；另一條線則是有人把「成本」與「正確性」逼到可量測、可證明——KV cache 的保溫帳、亂序處理器對弱記憶體 ISA 的形式驗證。
LLM 找到 Jacobian 猜想的反例，人類數學家負責驗證
有人用 Anthropic 的 Fable 模型在數學研究上產出了一個 Jacobian 猜想的候選反例——一個懸置近百年、三維以上原本連候選都沒有的問題。Kevin Buzzard 在部落格把這件事講成「人類數學家正在被反例打敗」。關鍵是分清楚兩件事：AI 負責生成 candidate，人類與工具負責驗證，這不等於「AI 自己證明了一切」（深入文章補上 Terence Tao 的獨立消化與第二來源）。
一整隊 Claude 併發寫出能編譯 Linux 的 C 編譯器
Anthropic 的工程團隊讓 16 個 Claude 實例併發協作，寫出一個約 10 萬行 Rust 的 C 編譯器，能跨多種架構編譯 Linux kernel。靠一個持續迴圈的 harness、用 git 同步各 agent、以 task lock 避免重工，前後跑了約 2,000 個 session、花了約 2 萬美元 API 費用，測試通過率達 99%，還建置出可開機的 Linux 6.9。文章也誠實記下缺口：程式碼生成效率與部分架構特性仍未補齊。
Kimi K3 與 Fable 幾乎並駕齊驅，分流路由才是真正的省錢招
Fireworks 測了約 1,030 個橫跨五類的 agentic 任務，發現 Kimi K3 與 Fable 幾乎打平——SWE 類 benchmark 上 K3 拿 92.4%、Fable 92.6%——但把兩者用 router 智慧分流後，整體準確率能推到 93%。更關鍵的是成本：K3 在五類 benchmark 全部更便宜，單用 K3 最多比單用 Fable 省下約 50 倍成本，oracle router 把 72–96% 的流量都導向 K3。
Prompt Design at Scale：指令一多、context 一長，模型就開始壞
一份跨五個模型的研究把 prompt 設計拆成三個變數來測：指令格式、同時下的指令數、context 長度。結論很硬：每個模型、每種格式、每個位置，完美回應率都在 N=80 條指令時歸零；context 一旦逼近上限，模型不是亂編（fabrication 為 0）而是大量拒答（refusal 從 0% 飆到 79–90%）。格式的好壞則因模型而異——markdown 沒有穩定優勢，某個 35B 模型用純文字反而更好，而換格式還會多吃 22–37% 的 token。
把亂序處理器形式驗證為合乎順序性的弱記憶體 ISA
一篇論文把一顆亂序（out-of-order）多處理器實作，形式驗證為滿足一個順序性（in-order）的弱記憶體模型 ISA 規格。難點在於亂序執行、投機與 store buffer 會讓記憶體操作的可見順序偏離程式順序，證明必須說明這些重排仍落在弱記憶體規格允許的範圍內。對想把形式方法帶進真實 CPU 驗證的人，這是一個把「實作 refine 規格」講清楚的案例。
Linux kernel 要支援 $ORIGIN 了——只是有點勉強
動態連結裡的 $ORIGIN 是一個會解析成執行檔所在目錄的 placeholder，讓二進位可以相對定位。Linux kernel 正在用 eBPF 版的 binfmt_misc，加上動態選擇 interpreter 的能力，讓像 Nix 這種需求能在執行期覆寫 PT_INTERP。「有點勉強」在於：傳統 binfmt_misc 交接會讓「註冊的 interpreter 變成那個 process」、破壞透明度，所以 kernel 另加了新的 dispatch 模式——特別是 loader substitution 的 L flag，只做 PT_INTERP override 而不換掉 process 身分。
KV cache 保溫的帳：keepalive 到底划不划算
一篇 arXiv 論文把 agentic 工作負載的一個老問題算清楚：多輪之間，prompt／KV cache 會被 provider 逐出，下一輪就得重算 prefill，成本與延遲雙漲。論文把 keepalive——週期性戳一下讓 cache 別被逐出——建成一個經濟學模型，算出各家的損益兩平閒置時長：Anthropic 約 46 分鐘、OpenAI 與 DeepSeek 約 36 分鐘、Google 只有約 12 分鐘。深入文章再對照 mempko 跨四家的實測，看同一組 keepalive 參數為什麼不能通用。
Justif：把出版級斷行與微排版帶進瀏覽器
Justif 是一個把出版級文字對齊帶進瀏覽器的示範工具：讓你即時對比瀏覽器原生的 justify 與它自己的排版，並逐一開關 hyphenation、protrusion（標點懸掛）、expansion、tracking、hang punctuation 等微排版特性，還附一個把畫面模糊化的 squint test 來檢查間距是否勻稱。這類最佳化斷行的想法可追到 Knuth-Plass，而它把「為什麼原生 justify 常常很醜」變成可以親手撥弄的東西。
用 Lean 做形式驗證入門：從 One-Time Pad 學起
一份給密碼工程師的教學，用 Lean 這個證明輔助器帶你寫出機器可檢查的數學證明，第一部分以形式驗證 One-Time Pad 當作實例。它從 bitstring 與 XOR 函式這些基礎切入，順帶介紹 Lean 的隱式參數、lambda 與 vector 型別等語法。定位很明確：寫給剛接觸形式驗證、或想複習基礎的密碼工程師。
GitHub 突然拒絕我的 SSH key——修法竟是補回一個 .pub 檔
作者的 GitHub SSH 認證突然失敗，追下去發現關鍵在那個看似無用的 .pub 公鑰檔：它會改變 OpenSSH 走哪一條認證流程——有 .pub 時 client 會先試探，沒有時 OpenSSH 直接送出完整簽章請求，而 GitHub 更新後的伺服器顯然會拒絕後者。修法是把公鑰補回來：ssh-keygen -y -f ~/.ssh/github_rsa > ~/.ssh/github_rsa.pub。