Mistral AI показала Leanstral: кодинг, который можно не проверять
habr.comФранцузская Mistral AI представила Leanstral – открытого ИИ-агента, который не просто генерирует, а ещё и формально доказывает корректность своих же творений.
Это помощник, который работает в связке с инструментом формального доказательства Lean 4. Его задача – помогать в “инженерии доказательств”, то есть строго проверять математические выкладки и программные спецификации.В Mistral рассудили здраво: зачем нам просто “умная” нейросеть?
