code completionではなくLean 4 proof engineeringを狙うagent

2026年3月16日、Hacker NewsではMistralのLeanstral公開が277 points、49 commentsを集めた。注目された理由は、Leanstralが汎用的なcoding chatbotとしてではなく、Lean 4 proof engineering向けのopen agentとして提示されている点にある。Mistralは、高リスクなsoftwareやmathematicsではmodelがcodeを書くこと自体よりも、その結果をhuman reviewで確認する工程が本当のボトルネックになっていると説明し、次の世代のcoding agentはimplementationとverificationを一体で扱うべきだと主張している。

launch postによれば、Leanstralはsparse architectureで6B active parametersを使い、weightsはApache 2.0 licenseで公開される。提供形態も広い。Mistral Vibe内のagent mode、free API endpointである labs-leanstral-2603、そしてself-host向けのopen weightsが用意される。さらにMCP workflowもサポートし、特に lean-lsp-mcp と組み合わせて高い性能を出せるよう学習したとされる。ここで重要なのは、単発のcode generationではなく、toolを回しながら証明可能な形で進めるworkflowに焦点があることだ。

evaluation sectionも技術的な見どころになっている。Mistralはisolatedな数学問題ではなく、実際のformal repository pull requestを完了できるかを見るFLTEvalを導入した。公開表ではLeanstral pass@2が26.3 scoreを記録し、Claude Sonnet 4.6の23.7を上回る一方、run costは$36とされ、Sonnetの$549よりかなり低い。pass@16では31.9まで伸びるが、それでもOpus級より低コストに留まる。さらにGLM5、Kimi、Qwenのようなより大きいopen-weight modelと比べても、active parameterの小ささに対して効率よく伸びると主張している。

Hacker Newsで反応が大きかったのはこの文脈だ。最近のcoding agent議論は、modelがどれだけ多くのcodeを書けるかより、どれだけ検証可能で再現可能な成果を返せるかへ移りつつある。Leanstralはopen-model ecosystemをverified implementationの方向へ押し出そうとする、かなり明確な試みと言える。benchmark claimには今後の外部検証が必要だとしても、communityが実際のLean repositoryで試せる具体物が出てきた意味は大きい。

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

#leanstral

Hacker Newsで注目のLeanstral、MistralがLean 4向けopen verified coding agentを公開