Leanstral 证明仅 6 行，碾压 Claude 与 Aristotle 的冗长输出

AlbertQJiang · x · 2026-08-19

在 ICML 2026 的“使用 Lean 和机器学习证明定理”教程中，展示了 Leanstral 模型的惊人能力。在特定任务中，Leanstral 生成了一个仅需 6 行代码的优雅证明，而 Claude 产生了 40-50 行的混乱代码，Aristotle 的 MCTS 追踪更是据说长达 180 行（需要三张竖屏截图才能显示完）。这一对比凸显了 Leanstral 在形式化验证和简洁推理方面的潜力。