Mistral推出開源模型Leanstral，專為Lean 4形式化證明工作流程設計
模型介紹與功能
法國AI公司Mistral AI推出開源模型Leanstral，專為Lean 4形式化證明工作流程設計，並以程式碼代理形式提供服務。該模型不僅能生成程式碼，還能處理形式化證明相關任務。
授權與整合
Leanstral的模型權重以Apache 2.0授權釋出，可整合至Mistral Vibe代理模式中，讓開發者能更便捷地使用。
實驗性API與使用方式
官方提供labs-leanstral-2603實驗性API端點，開發者可透過雲端或自建環境使用此模型，進行形式化證明與程式碼生成任務。