Lean 4와 proof engineering에 초점을 맞춘 coding agent

2026년 3월 16일 Hacker News에서는 Mistral의 Leanstral 공개가 277 points와 49 comments를 기록하며 빠르게 부각됐다. 이 발표가 흥미로운 이유는 Leanstral이 일반적인 code generation model이 아니라 Lean 4 proof assistant를 위한 open agent라는 점에 있다. Mistral은 high-stakes software와 mathematics에서는 model output 자체보다 human review가 더 큰 병목이 되며, 다음 단계의 coding agent는 구현뿐 아니라 proof와 verification까지 다뤄야 한다고 설명한다.

source page에 따르면 Leanstral은 sparse architecture 위에서 6B active parameters를 사용하고, weights를 Apache 2.0 license로 공개한다. 배포 방식도 단순하지 않다. Mistral Vibe 안의 agent mode, free API endpoint labs-leanstral-2603, 그리고 자체 실행용 open weights를 함께 제공한다. 여기에 MCP 지원을 붙이고, 특히 lean-lsp-mcp와 함께 높은 성능을 내도록 학습시켰다는 설명도 포함됐다. 핵심 메시지는 coding agent를 chat interface가 아니라 verifiable workflow로 옮기겠다는 것이다.

benchmark도 커뮤니티가 관심을 가질 만하다. Mistral은 isolated math problem 대신 실제 formal repository pull request를 기준으로 한 FLTEval을 제시했고, Leanstral pass@2가 26.3 score를 기록하면서 Claude Sonnet 4.6의 23.7을 넘어섰다고 밝혔다. 공개된 표에서는 Leanstral pass@2의 실행 비용을 $36, Sonnet을 $549, Opus를 $1,650로 제시한다. pass@16에서는 Leanstral이 31.9까지 올라가지만, 여전히 Opus보다 훨씬 낮은 비용대에 남아 있다. 또한 GLM5, Kimi, Qwen 같은 large open models와 비교해도 훨씬 작은 active parameter 규모로 경쟁력 있는 결과를 냈다고 주장한다.

Hacker News에서 이 글이 반응을 얻은 이유도 분명하다. 최근 coding agent 논의는 '코드를 얼마나 많이 쓰는가'보다 '결과를 얼마나 검증 가능한 형태로 내놓는가' 쪽으로 이동하고 있다. Leanstral은 그 흐름을 가장 직접적으로 겨냥한다. formal proof repository와 software specification을 동시에 겨냥한 open model이 실제 workflow에 들어오면, code review의 부담을 줄이는 방식도 달라질 수 있다.

Primary source: Mistral Leanstral announcement. Community discussion: Hacker News.

#leanstral

Hacker News가 주목한 Leanstral, Mistral의 Lean 4용 open verified coding agent