Mistral은 2026년 3월 16일 Leanstral을 공개하며 이를 Lean 4를 위해 설계한 첫 오픈소스 코드 에이전트라고 소개했다. Lean 4는 정형 검증과 정리 증명에 널리 쓰이는 proof assistant로, 일반적인 coding assistant를 그대로 가져와 적용하기보다 저장소 수준의 실제 formal workflow에 맞춘 전용 모델이 필요하다는 것이 이번 발표의 출발점이다.

회사 설명에 따르면 Leanstral의 핵심은 규모 경쟁이 아니라 효율성과 작업 적합성이다. Mistral은 이 모델이 6B active parameters로 동작하며, 단일 수학 문제 풀이보다 실제 formal repository에서 작업하도록 학습됐다고 밝혔다. 또 competition math 중심 평가에서 벗어나기 위해 새로운 평가군인 FLTEval과 기술 보고서도 함께 예고했다.

Lean 4 전용 오픈소스 code agent
Apache 2.0 라이선스로 가중치 공개
Mistral Vibe에 통합되고 labs-leanstral-2603 API로도 제공
공개된 비교에서 FLTEval 기준 더 큰 오픈소스 모델 대비 효율 우위를 주장

Mistral은 공개된 비교에서 Leanstral이 FLTEval에서 높은 효율을 보였다고 설명했다. 게시물에는 Leanstral이 더 큰 open-source peer와 비교해 적은 계산량으로 경쟁력 있는 결과를 냈고, 추가 pass를 허용했을 때 성능이 더 올라가는 모습이 제시됐다. 메시지는 분명하다. formal methods와 verified code workflow는 더 큰 general model 하나로 해결하기보다, 작업 구조에 맞춘 agent 설계가 더 중요하다는 것이다.

출시 방식도 실용적이다. 사용자는 Mistral Vibe에서 바로 모델을 호출할 수 있고, 한시적으로 접근성을 높인 API endpoint를 통해 테스트할 수도 있으며, 가중치를 직접 내려받아 자체 인프라에서 실행할 수도 있다. 정형 검증, theorem proving, 안전성이 중요한 code generation 수요가 커지는 시점에서 Leanstral은 open model 진영이 trustworthy code tooling을 어떻게 제품화하려는지 보여주는 사례다.

#code-agents

Mistral, Lean 4 전용 오픈소스 코드 에이전트 Leanstral 공개