2026-06-11 formal-verification
Opus 4.8 一次跑出带证明的算法:形式化验证正在变成模型的硬基准
一名开发者用 Opus 4.8 自主跑出了一份带 Lean 形式化证明的多边形求交算法,此前的模型做不到。证明要么成立要么不成立,这比刷分诚实,但一个案例不等于普遍能力。
阅读全文coding
High-signal frontier AI context tagged with coding.
2026-06-10 cohere
Cohere North Mini Code:开放权重编码模型的竞争,正在从拼规模转向「能不能单卡自托管 + 许可证够不够干净」
Cohere 这家一向做封闭企业模型的公司,首次拿出面向开发者的 agentic 编码模型:30B MoE(3B active)、Apache 2.0、单张 H100 就能跑。比起 33.4 的 Coding Index 分数,更值得 builder 记住的是它押的方向——主权自托管。
阅读全文