Leanstral 1.5 是一款采用 Apache-2.0 许可的免费模型，拥有 6B 激活参数，在形式化验证方面实现了重大性能升级，在 miniF2F 上达到饱和，解决了 587/672 道 PutnamBench 问题，并在 FATE-H（87%）和 FATE-X（34%）上取得了最先进的结果。
该模型通过中期训练、监督微调和基于 CISPO 的强化学习进行训练，在智能体证明工程和真实世界代码验证方面表现出色，在测试的 57 个代码仓库中发现了 5 个此前未知的 bug。Leanstral 1.5 完全开源，可通过 Hugging Face 和免费 API 获取，现已可用于 Lean 4 中的实际证明工程。
自发布以来，Leanstral 为 Lean 4 中的证明工程提供了一种开放且实用的方法。今天，我们发布 Leanstral 1.5，这是一款采用 Apache-2.0 许可的免费模型，总参数 119B，激活参数仅 6B，带来的性能升级使形式化验证比以往任何时候都更强大、更易获取。
Leanstral 1.5 **在 miniF2F 上达到饱和，解决了 587/672 道 PutnamBench 问题，**并在 FATE-H 上达到 87%、FATE-X 上达到 34% 的新最先进水平。除基准测试外，它还能验证复杂的代码属性，并在开源代码仓库中发现此前未知的 bug——证明严格的形式化方法在真实世界应用中既有效又实用。
训练 Leanstral
Leanstral 1.5 经历三个阶段：中期训练、监督微调，以及使用 CISPO 的强化学习。Leanstral 1.5 依托在两个强化学习环境上的大规模训练：
在 多轮环境中，模型会收到一个定理陈述，必须证明或证伪它。模型提交一个证明，接收 Lean 编译器的反馈，并在每次尝试中改进其方法。如果证明通过编译，它就成功了；否则循环继续，直到模型要么解决问题，要么耗尽预算。
在 代码智能体环境中，Leanstral 就像一个在原始文件系统中工作的开发者：它编辑文件、运行 bash 命令，并使用 Lean 语言服务器实时检查目标、错误和类型信息。这使它能够处理长周期任务，例如完成代码库中的部分证明、构建辅助引理，并在多轮上下文压缩中持续坚持。模型学会驾驭完整的证明工程工作流，最终由 我们分叉的 SafeVerify 针对一组目标定理进行正确性验证。
评估
我们在以下基准上评估 Leanstral：
miniF2F 是一个面向形式化数学的跨系统基准，涵盖从初等题目到 IMO 级别的挑战，测试代数、组合数学和数论等多方面的证明能力。
PutnamBench 由 672 道 Putnam 数学竞赛题目组成，需要深度推理和长证明链来求解这些具有挑战性的数学问题。
FATE-H 和 FATE-X 分别是面向研究生和博士级别问题的抽象代数基准，测试群论、环论和模论等领域的高级推理能力。
FLTEval 基于费马大定理代码仓库中的真实 pull request，测试具有真实世界复杂度的实用证明工程能力。
我们在 miniF2F 上完全饱和，验证集和测试集均达到 100%。在 PutnamBench 和 FATE-H/X 上，我们将 Leanstral 1.5 与无自然语言引导的 Goedel-Architect、高配置下的 Seed-Prover 1.5 以及 AxProverBase 进行了对比。
Leanstral 在 FATE-H/X 上达到新的 SOTA，分别解决了 87 道和 34 道问题。在 PutnamBench 上，它以远更低的成本以多解出 7 道问题的优势胜过高配置的 Seed-Prover 1.5：每道问题约 $4，而 Seed-Prover 估计需要 $300 或更多，其高配置每道问题的运行预算为 10 H20-days。
排名更高的证明器仅在不同的条件下运行——有些接受自然语言证明引导，另一些运行成本远更高，例如 Aleph Prover 每道问题 $54–68。
Leanstral 1.5 展现出我们在形式化推理模型上所见过的最强测试时扩展能力。下图追踪了 PutnamBench 上的 Pass@8，随着我们将每次尝试的 token 预算从 25k 提升到 4M：性能全程平滑且单调地攀升，从 50k 时解出 44 道题，到 200k 时解出 244 道，1M 时解出 493 道，4M 时解出 587 道。
当证明变得冗长时，Leanstral 不会放弃，而是持续推理、编辑文件，并在数百万 token 的跨度内反复修订，将这份预算直接转化为解出的题目——下方 AVL 树证明背后的行为正是如此，它在 22 次压缩中运行了超过 270 万 token。
伴随此次发布，我们还完全开源了 FLTEval。Leanstral 1.5 将该基准上的 pass@1 从 21.9 提升到 28.9，pass@8 从 31.9 提升到 43.2，以七分之一的成本超越了 Opus 4.6 的 39.6。如下方图表所示，它还扩大了对规模大 3–10 倍的开源模型的领先优势。
代码验证案例研究
尽管主要针对数学进行训练，Leanstral 1.5 在代码验证方面展现出强大的能力。我们呈现 2 个关键案例研究，以展示其影响力。
AVL 树：证明时间复杂度
AVL 树是自平衡二叉搜索树，通过在插入和删除过程中重新平衡来维持 O(log n) 的高度。Leanstral 1.5 为一个真实实现证明了这些时间复杂度保证——这项任务需要结构归纳来对应树的递归结构、谨慎处理单子式时间追踪，以及对重平衡路径进行穷尽式情况分析。
在超过 270 万个 token 和 22 次压缩过程中，Leanstral 系统性地逐层展开 TimeM 单子，揭示出底层计算，尽管它们与控制流相互交织。它确立了插入操作每单位高度 48 步加一个常数的近乎紧确的界，随后通过对数关系将高度与树的大小联系起来，给出了完整、经过验证的证明，证明插入和删除确实是 O(log n)。
缺陷发现：找出隐藏的缺陷
为了测试 Leanstral 的缺陷捕捉能力，我们构建了一条自动化流水线：Aeneas 将 Rust 代码转换为 Lean，而 Leanstral 则推断用户意图并根据代码生成正确性属性。随后 Leanstral 尝试对每个属性进行四次证明。
如果全部失败，它会转而尝试证明其否定命题，同样进行四次尝试。在 57 个受测代码仓库中，这一流程标记出 47 个被违反的属性，其中 11 个指向真正的缺陷——其中 5 个此前未在 GitHub 上被报告过。
其中一个 bug 出现在 datrs/varinteger 库 zigzag 解码的符号函数中。当输入为 Std.U64.MAX 时，表达式 (value + 1) 发生溢出，导致调试模式下崩溃，发布模式下则出现静默数据损坏——这是一个测试和模糊测试通常难以发现的边缘情况。Leanstral 的流水线自动捕获了它，表明形式化验证已经可以应用于真实世界的代码库，并发现一些传统方法所忽略的 bug。
Leanstral 1.5 采用 Apache-2.0 许可证。权重可在 Huggingface 上找到，同时现在也已 作为免费 API 端点 提供，即 leanstral-1-5。我们推荐在 Mistral Vibe 中使用它。要开始你的旅程，请获取一个 API Key，然后：
1. 设置 Mistral Vibe
uv tool install mistral-vibeuv tool update mistral-vibevibe --setup
2. 安装 Leanstral 1.5
/leanstallexit
3. 启动智能体
vibe --agent lean
4. 安装 Lean LSP MCP（可选）
强烈建议安装 Lean LSP MCP，方法是将以下内容添加到你的 ~/.vibe/config.toml
[[mcp_servers]]name = "lean-lsp"transport = "stdio"command = "uvx"args = ["lean-lsp-mcp"]tool_timeout_sec = 600
如果不存在现有的 MCP 服务器，你可能需要移除 mcp_servers = []。
5. 开始证明
让 Leanstral 去攻克一个定理、调试一个证明，或为某个代码仓库做出贡献。就这么简单。
Leanstral 1.5, a free Apache-2.0 licensed model with 6B active parameters, delivers a major performance upgrade in formal verification, saturating miniF2F, solving 587/672 PutnamBench problems, and achieving state-of-the-art results on FATE-H (87%) and FATE-X (34%). Trained through mid-training, supervised fine-tuning, and reinforcement learning with CISPO, it excels in agentic proof engineering and real-world code verification, uncovering 5 previously unknown bugs across 57 repositories tested. Fully open-sourced and available via Hugging Face and a free API, Leanstral 1.5 is now accessible for practical proof engineering in Lean 4.
Since its launch, Leanstral has offered an open, practical approach to proof engineering in Lean 4. Today, we are releasing Leanstral 1.5, a free Apache-2.0 licensed model with 119B total and only 6B active parameters, delivering a performance upgrade that makes formal verification more powerful and accessible than ever.
Leanstral 1.5 **saturates miniF2F,solves587/672 PutnamBench problems,**and achieves a new state-of-the-art of %87 on FATE-H and 34% on FATE-X. Beyond benchmarks, it verifies complex code properties and uncovers previously unknown bugs in open-source repositories—proving that rigorous formal methods can be both effective and practical for real-world use.
Training Leanstral
Leanstral 1.5 goes through a three-stage process: mid-training, supervised fine-tuning, and reinforcement learning with CISPO. Leanstral 1.5 leverages extensive training on two RL environments:
In the multiturn environment, the model is given a theorem statement and must either prove or disprove it. The model submits a proof, receives Lean compiler feedback, and refines its approach with each attempt. If the proof compiles it succeeds; otherwise the loop continues until the model either solves the problem or exhausts its budget.
In the code agent environment, Leanstral operates like a developer in a raw filesystem: it edits files, runs bash commands, and uses the Lean language server to inspect goals, errors, and type information in real time. This allows it to tackle long-horizon tasks like completing partial proofs in a repository, building auxiliary lemmas, and persisting through multiple rounds of context compaction. The model learns to navigate the full proof-engineering workflow and is finally verified by our fork of SafeVerify for correctness given a list of target theorems.
Evaluation
We evaluate Leanstral on the following benchmarks:
miniF2F is a cross-system benchmark for formal mathematics, ranging from elementary problems to IMO-level challenges, testing diverse proof abilities across algebra, combinatorics, and number theory.
PutnamBench consists of 672 problems from the Putnam Mathematical Competition, requiring deep reasoning and long proof chains to solve challenging mathematical problems.
FATE-H and FATE-X are abstract algebra benchmarks for graduate and PhD-level problems, respectively, testing advanced reasoning in areas like group theory, ring theory, and module theory.
FLTEval is based on real pull requests from the Fermat’s Last Theorem repository, testing practical proof engineering with real-world complexity.
We saturate miniF2F completely, reaching 100% on both the validation and test sets. On PutnamBench and FATE-H/X, we compare Leanstral 1.5 against Goedel-Architect without natural-language guidance, Seed-Prover 1.5 at its high setting, and AxProverBase. Leanstral reaches a new state-of-the-art on FATE-H/X, solving 87 and 34 problems respectively. On PutnamBench, it edges out Seed-Prover 1.5 high by 7 problems at far lower cost: about $4 per problem, against an estimated $300 or more for Seed-Prover, whose high setting runs with a budget of 10 H20-days per problem. The only provers ranked higher operate under different conditions—some receive natural-language proof guidance, others cost far more to run, like Aleph Prover at $54–68 per problem.
Leanstral 1.5 shows the strongest test-time scaling we have seen from a formal-reasoning model. The figure below tracks Pass@8 on PutnamBench as we raise the token budget per attempt from 25k to 4M: performance climbs smoothly and monotonically the whole way, from 44 problems solved at 50k to 244 at 200k, 493 at 1M, and 587 at 4M. Rather than giving up when a proof runs long, Leanstral keeps reasoning, editing files, and revising across millions of tokens, turning that budget directly into solved problems—the same behavior behind the AVL-tree proof below, which ran for over 2.7 million tokens across 22 compactions.
With this release, we also fully open source FLTEval. Leanstral 1.5 lifts pass@1 on the benchmark from 21.9 to 28.9 and pass@8 from 31.9 to 43.2, surpassing Opus 4.6's 39.6 at one-seventh the cost. It also widens its lead over open-source models 3–10× larger, as shown in the figure below.
Code Verification Case Studies
While being primarily trained for mathematics, Leanstral 1.5 exhibits strong abilities in code verification. We present 2 critical case studies to demonstrate its impact.
AVL Trees: Proving Time Complexity
AVL trees are self-balancing binary search trees that maintain O(log n) height through rebalancing during insertions and deletions. Leanstral 1.5 proved these time complexity guarantees for a real implementation—a task that required structural induction to mirror the tree’s recursive structure, careful handling of monadic time tracking, and exhaustive case analysis for rebalancing paths. Over 2.7 million tokens and 22 compactions, Leanstral systematically unfolded each layer of the TimeM monad, exposing the underlying computations despite their interleaving with control flow. It established an almost tight bound of 48 steps per height unit plus a constant for insertion, then connected height to tree size via a logarithmic relationship, delivering complete, verified proofs that insertion and deletion are indeed O(log n).
Bug Discovery: Finding Hidden Flaws
To test Leanstral’s bug-catching abilities, we built an automated pipeline: Aeneas translates Rust code to Lean, while Leanstral infers the user intent and generates correctness properties from the code. Leanstral then attempts to prove each property in four attempts. If they all fail, it tries to prove the negation instead, also with four attempts. Across 57 tested repositories, this process flagged 47 violated properties, with 11 pointing to genuine bugs—5 of them previously unreported on GitHub.
One such bug was in the sign function for zigzag decoding of the datrs/varinteger library. On input Std.U64.MAX, the expression (value + 1) overflowed, causing crashes in debug mode and silent corruption in release mode—an edge case that testing and fuzzing would typically miss. Leanstral’s pipeline caught it automatically, demonstrating that formal verification can already be applied to real-world codebases and find bugs that some traditional methods overlook.
Leanstral 1.5 has a Apache-2.0license. The weights can be found on Huggingface, while also being available now as a free API endpoint as leanstral-1-5. We recommend using it in Mistral Vibe. To begin your journey, grab an API Key, and:
1. Set up Mistral Vibe
uv tool install mistral-vibeuv tool update mistral-vibevibe --setup
2. Install Leanstral 1.5
/leanstallexit
3. Launch the agent
vibe --agent lean
4. Install Lean LSP MCP (Optional)
It is highly recommended to install Lean LSP MCP by adding the following to your ~/.vibe/config.toml
[[mcp_servers]]name = "lean-lsp"transport = "stdio"command = "uvx"args = ["lean-lsp-mcp"]tool_timeout_sec = 600
If there are no existing MCP servers, you may have to remove mcp_servers = [].
5. Start proving
Ask Leanstral to tackle a theorem, debug a proof, or contribute to a repository. It’s that simple.