Mistral, Leanstral-1.5-119B-A6B 공개

솔직히 말해서, Lean4는 "결점이 없는 하스켈" 정도로 볼 수 있음 (물론 이건 엄청난 단순화고, 지연 평가 같은 하스켈만의 독특하고 강력한 기능들, 그리고 개인적으로 훌륭하다고 생각하는 하스켈 생태계에 대한 모욕이 될 수도 있겠지만!). 만약 하스켈을 알아볼 생각이었다면, 대신 Lean4를 먼저 살펴보는 것도 고려해 볼 만함. 설치하자마자 바로 잘 작동하는 경험을 할 수 있고(하스켈도 평판보다는 훨씬 낫지만), 모든 걸 무시하고 시작하기에도 충분히 괜찮음...

vibethinker랑 비슷하네. 3B인데 수학 괴물인 모델 말이야. 물론 툴 콜링 능력은 사실상 프롬프트 가이드에 의존하지만.

그냥 Qwen 27B나 Gemma 4한테 물어보는 거랑 비교해서 이걸로 수학 에이전트를 만드는 게 무슨 이점이 있을까?

Lean은 함수형 언어라 일반적인 코딩 작업에도 많이 쓰이고 Rust랑도 궁합이 잘 맞음.