evaluation

Opus 4.8 一次跑出带证明的算法:形式化验证正在变成模型的硬基准

一名开发者用 Opus 4.8 自主跑出了一份带 Lean 形式化证明的多边形求交算法,此前的模型做不到。证明要么成立要么不成立,这比刷分诚实,但一个案例不等于普遍能力。