Open Source AI
Leanstral 1.5 выводит открытые кодовые модели в сторону формальной верификации
Свежая пара релизов на Hugging Face показывает, как открытый ИИ уходит от общего разговора к узким рабочим задачам. Mistral выпустила Leanstral 1.5 для доказательств в Lean 4, а Poolside — Laguna XS 2.1-FP8, которая обещает агентную разработку с длинным контекстом на более доступном железе.