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