We’re releasing ProofBench, a new benchmark evaluating whether models can write formally verified mathematical proofs. Unlike natural language math benchmarks where subtle errors can go unnoticed, ProofBench requires proofs that are machine-checkable; either a solution compiles or it doesn’t.

• Aristotle, a system from Harmonic, achieved the best performance at 71%, roughly 2x the score of the best foundation model.
• Foundation models struggle significantly withs formal proof generation. Claude Opus 4.5 (Thinking) leads foundation models at 36%, followed by Gemini 3 Pro (11/25) at 20% and Claude Sonnet 4.5 (Thinking) at 19%.
• Problems are drawn from advanced undergraduate and graduate-level mathematics, spanning probability theory, measure theory, analysis, algebra, algebraic geometry, and number theory.
• While specialized tools like Aristotle show promise for assisting with formal mathematics, the large gap in foundation model performance highlights significant room for improvement in reliable formal reasoning.

We’ve finished our evaluation of Kimi K2.5 and continue to find excellent performance across the board. Here are some highlights:

• The model places first on CorpFin by a significant margin (2%), though it takes substantially longer to respond than other models in the top 10.
• The model is remarkably consistent - its worst placement is 16th, on CaseLaw, on which it remains within 10% of first place.
• The model is head and shoulders above its open-weight competition, placing first among open-weight models on 13 of the 17 benchmarks on which it was evaluated.

We ran all benchmarks on the native provider with temperature 1 as recommended by Kimi, with 128K max tokens on all but the coding benchmarks, for which we used 256K.

Stay tuned for our evaluation on Vibe Code Bench and congrats again to Moonshot on the release!

Kimi K2.5 is the new #1 open-weight model, taking the top spot on both our Vals Index and our Vals Multimodal Index. Here are the key takeaways:

• Like it’s predecessor Kimi K2 Thinking, the model excels across coding tasks, placing first across open-weight models on both SWE Bench and Terminal Bench 2.
• Unlike its predecessor, it also excels on our Finance Agent and SAGE, placing third across all models on the latter. By comparison, Kimi K2 Thinking didn’t even support multimodal input!
• Aside from being open-weight, another significant differentiation between Kimi and other top models is price - it’s the cheapest model in the top 10 of both Vals indices!

We ran all benchmarks on the native provider with temperature 1 as recommended by Kimi, with 128K max tokens on all but the coding benchmarks, for which we used 256K.

We’ve upgraded our Terminal-Bench evaluation to version 2. The new benchmark features more, better, and more relevant tasks.

Here are some key takeaways from our results:

• Claude Opus 4.5 (Nonthinking) leads the way on performance, scoring over 3% above its nearest competitor, Gemini 3 Pro (11/25). Surprisingly, its thinking variant Claude Opus 4.5 (Thinking), lags 4.5% behind in third place.
• We found that Gemini 3 Flash (12/25) demonstrates the most cost-effective performance, playing fourth at less than a fifth of the cost of the Claude models!
• GPT 5.2 and Grok 4 also demonstrate strong performance, as well as open-source offerings like MiniMax-M2.1 and GLM 4.7.