6B参数，吊打千亿级对手
一条看似普通的新闻，却藏着AI编程圈最劲爆的暗战。
Mistral AI刚刚发布了一个叫Leanstral的开源模型。参数规模？120B。但活跃参数只有6B。翻译成人话：这相当于你雇了一个能扛千亿级工作的实习生，干活利索，还只吃6B的饭量。
更狠的是价格。
在FLTEval基准测试中，Leanstral用两次尝试（pass@2）拿到26.3分，超过了Claude Sonnet的23.7。成本多少？36美元。Sonnet多少？549美元。16倍的价格差。
如果把次数拉满到16次尝试，Leanstral得分31.9，还是打不过Claude Opus 4.6的39.6。但你猜 Opus 要多少钱？1650美元。接近Leanstral的50倍。
说实话，这个对比有点"不讲武德"。 Opus确实更强，但强到值得多花45倍价格吗？
人类审核，成了最大的瓶颈
为什么Mistral要死磕这个赛道？
因为AI写代码这件事，正在撞上一堵墙。代码生成能力已经很强了，但高风险领域用不上。航空航天、医疗系统、加密算法——这些地方AI生成的代码，人类专家不敢信。
审代码太慢了。一个复杂的数学证明，专业人士可能要看几天。AI一天能生成十万行代码，人类审得过来吗？
Leanstral的解题思路很清奇：与其让AI生成代码再让人审，不如让AI生成代码+证明。代码不仅能跑，还能用数学方法自证"我确实解决了这个问题"。
这就不是"辅助编程"了，是"编程+审计"二合一。
真实案例：它真的在解决问题
官方秀了两个让我印象深刻的肌肉。
第一个是Stack Exchange的求助帖。有人升级Lean到4.29.0-rc6后，代码突然编译报错。问题很刁钻：一个简单的类型别名定义def T2 := List Bool，居然把rw tactic搞崩了。
Leanstral的操作很程序员：先复现问题，再建测试环境，最后定位到"def创建的是刚性定义，需要显式展开"。解决方案？把def换成abbrev。一行代码的事。
第二个案例更硬核。Leanstral直接把Coq（另一种证明助手）的定义翻译成Lean，还顺手证明了几个性质。没有人工干预，自己搞定。
这让我想起Simon Willison提过的"Red Green TDD"模式：AI不是直接给你答案，而是像资深开发者一样，先写测试，再定位问题，最后修复。
开源，真开源
评论区有人质疑：又来这套"开源"，怕不是又是套壳营销？
但这次好像不太一样。Leanstral的权重确实用的是Apache 2.0许可证，可以商用，可以修改，可以分发。不是"我们开源了但核心不给你"的那种。
当然，也有人唱反调："我身边没一个人用Mistral的模型。"这话不假。Claude和GPT在开发者心智里确实占主导。
但价格摆在那。36美元 vs 549美元，对小团队和个人开发者来说，这不是选择题，是生存题。
一个问题值得思考
评论区有人问了个很实在的问题：既然多轮尝试效果会递减，那下一轮换个模型会不会更好？比如第一轮用Leanstral，第二轮换Kimi，第三轮换Qwen，最后再用Leanstral收尾？
目前没人验证过。但这恰恰点出了一个关键点：AI编程工具的玩法，可能正在从"单点突破"转向"组合拳"。
而Leanstral最大的意义，可能是给这场游戏增加了一个新变量——一个便宜、开源、还能自证清白的选项。
至于它能不能干翻Claude全家？
答案可能不重要。重要的是，Claude终于有压力了。
【MiniMax-M2.1锐评】：Mistral这波操作很聪明——不正面硬刚GPT-4o和Claude Opus，而是切进"正式验证"这个细分赛道，用开源+低价精准爆破。AI编程的军备竞赛，才刚刚开始。
参考链接：
https://mistral.ai/news/leanstral