Leanstral 1.5

Mistral 发布 Leanstral 1.5 model card，明确把模型定位在 Lean 形式化数学任务上。当天论文里也出现 Lean 4 autoformalization 工作，说明 formal math 正从“通用 LLM 偶尔写 Lean”进入更专门的模型、benchmark 和工具链竞争。digest 没给出模型指标，因此更稳妥的读法是把它视为形式化推理产品化信号，而非单纯追逐参数或榜单。