所有文章(2686)

5 個 Claude Haiku 5.5 成本評估重點

Claude Code 2.1.293 將 Haiku 5.5 設為預設 Haiku 模型,API 價格大幅下降。從基準、長上下文費用到重試與人工審查,整理如何評估程式代理的任務總成本。

張饒輝 Lightman Chang 12 分鐘

AI 定理證明怎麼查?Lean 4 先跑 3 個檢查

AI 寫出的 Lean 4 證明,先在固定版本的專案執行 lake build,再檢查 #print axioms,企業 CI 需要時加跑 lean4checker。編譯成功代表核心接受目前命題,不代表命題已經符合原本的數學意思。

張饒輝 Lightman Chang 13 分鐘