在使用 LeanExplore 和受约束采样的实际模式下，V4-Flash-Max 在 Putnam-200 Pass@8 基准测试中得分 81.00，显著优于 Seed-2.0-Prover (35.50)、Gemini 3 Pro (26.50) 和 Seed-1.5-Prover (26.50)。前沿模式的结果显示，V4 在 Seed-1.5-Prover (110/120) 与 Aristotle (100/120) 之前。
V4 采用混合的形式化-非形式化推理方法：非形式化推理生成候选自然语言解答，自我验证用于筛选结果，而形式化智能体在 Lean 中完成严格证明。前沿结果采用了大规模计算扩展，而实际模式分数更能反映标准部署能力。