Mistral发布开源模型Leanstral-1.5-119B-A6B，专注形式验证与定理证明，在miniF2F、PutnamBench等测试中表现卓越。网友指出该模型并非通用或编程模型，而是专为Lean 4编程语言和数学证明优化的智能体，可用于自动定理证明和代码正确性验证。