- lueluelue2026-09-11
但是
- 输出 Token： 10,029,109 ÷ 21,560 ≈ 465.2 倍
- 输入 Token： 798,849,013 ÷ 1,138,635 ≈ 701.6 倍
而且证明极不美观，他最终写出来的证明代码平均是Astra的6倍
更新：Mistral工作人员说只有大概2%是Kimi
主楼 - 42-linuxdo2026-09-11
所以cost将会达到什么逆天量呢
- 不要吃太饱2026-09-11
硬凹出来啊，消耗这么多token
- NXDOMAIN2026-09-11
- Q_A2026-09-11
cost直接N/A，而且leanstral+别的模型呢
- 臻至2026-09-11
这是那个Lean榜嘛？Leanstral 1.5是Lean专项模型吧。PutnamBench Leaderboard 。
Kimi还有1m上下文，1+1>2 术业有专攻。不过这也太费了吧（
这么多Token应该像是Kimi 反复读.lean造成的。
- lueluelue2026-09-11
啊对，Lean榜，我订正一下去！
- k_ivring2026-09-12
现在gpt6可以用了吗？感觉太逆天了