# Mistral 发布 Leanstral 1.5，面向 Lean 4 证明工程的开源模型

- 来源：🚨 AI News | TestingCatalog (@testingcatalog)
- 发布时间：2026-07-04 20:57
- AIHOT 分数：56
- AIHOT 链接：https://aihot.virxact.com/items/cmr6dqd1o022rslf0lx2hgrux
- 原文链接：https://x.com/testingcatalog/status/2073390642344984674

## AI 摘要

Mistral 发布了 Leanstral 1.5，一个面向 Lean 4 证明工程的最新开源模型，权重已上传至 Hugging Face。Lean 4 既可用作通用函数式语言（开发 CLI 工具和库），也可作为证明助手机械验证代码、协议和算法的性质。引用数据显示，Leanstral 1.5 展示了形式化推理模型中最强的 test-time scaling：在 PutnamBench 上，Pass@8 随 token budget 从 25k 提升至 4M 持续稳定增长。

## 正文

ICYMI： Mistral released Leanstral 1.5， a SOTA open model for Lean 4 proof engineering.

> Developers use Lean 4 as a general-purpose functional language （for CLI tools and libraries） and as a proof assistant to mechanically verify properties of code， protocols， and algorithms.

Weights are on Huggingface 👀

### 引用推文

> Mert Ünsal：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 to...