Leanstral 1.5是Mistral AI发布的新模型，在保持高效推理的同时提升了性能，适用于多种自然语言处理任务。

Mistral AI 发布了 Leanstral 1.5 模型，这是一个针对 Lean 4 形式化证明工程优化的更新版本，主要用于自动化定理证明和自动形式化。该模型总参数量为 119B，但实际激活参数仅为 6.5B，支持 256k 的上下文长度，且使用价格为 0 美元。它具备多种功能，包括聊天补全、函数调用、智能体与对话、内置工具、结构化输出、预测输出、前缀补全、OCR 处理、文档问答、FIM 补全、嵌入、审核、音频转录与合成、时间戳以及批处理等。此外，页面还列出了其他相关模型，如 Mistral Medium 3.5、Voxtral TTS 和 Mistral Small 4，并提供了 Mistral AI 的各类链接，包括关于我们、客户、职业、联系方式、AI 解决方案、合作伙伴、研究、文档、大使、食谱、Studio、Vibe、Mistral Code、Mistral Compute、API 试用、法律条款、隐私政策、社区渠道等。

根据评论内容，主要观点如下：

观点一：对Mistral模型实际性能的质疑 - 评论者doctorpangloss质疑Mistral模型是否真正在客观指标上表现最佳，还是仅因“欧盟背景”被使用。 - 关键引用："does anyone use anything from Mistral because it performs the best... or is it only used 'because EU'?"（“有人是因为Mistral性能最佳而使用它吗？还是仅仅因为‘欧盟’？”） - 关键引用："I wonder if anyone has observed it perform better on any objective metric in any rigorous setting."（“我想知道是否有人在任何严格环境中观察到它在任何客观指标上表现更好。”）

观点二：对Leanstral 1用途的疑问 - 评论者esafak询问该工具是否仅适用于定理证明，还是也能用于程序规范。 - 关键引用："Is this useful for specifying programs too or only theorems?"（“这对指定程序也有用，还是仅适用于定理？”）

总结：评论主要围绕Leanstral 1（Mistral相关工具）的实际性能与用途展开，一方质疑其客观优势，另一方关注其应用范围。目前无评分数据，观点呈现平衡性。