Lean 4エンジニア必見！オープンソースのAIコードエージェント「Leanstral」が登場

Lean 4での開発や定理証明を加速させる、オープンソースの専用AIコードエージェント「Leanstral」がリリースされました。Lean 4に特化して設計されているため、より正確で効率的なコーディング支援が期待できます。Leanコミュニティ注目のツールです！

信頼できる「バイブ・コーディング」だ。あっちの類よりずっとマシ！

とはいえ、比較については正直よく分からないな。Haikuに対するコスト削減を強調してるけど、Haikuはこのタスクがあまり得意じゃないし、Leanstralはさらに性能が低いんだろ？正確性を最適化しようとしてるなら、「性能は悪いけど10倍安い」なんて話が関係あるのか？それとも僕が何か勘違いしてる？

有望な点としては、Opusもこのベンチマークではそれほど良くないから、これをスケールアップすればOpusを超える結果が出せるかもしれない。そこが今回の重要なポイントなんだろうな。

僕と同じ反応をした人が他にいるか気になるんだけど。

このモデルはこのタスク専用にトレーニングされてるのに、Opusにかなり1負けてる。

Opusのコストは約6倍。でも、このタスクの内容を考えれば……間違いなく払う価値があると思う。

彼らが報告している実世界での成功例を見ると、サイモン・ウィリソンの「Red Green TDD」を思い出すよ。 https://simonwillison.net/guides/agentic-engineering-pattern... (https://simonwillison.net/guides/agentic-engineering-patterns/red-green-tdd/)

暗中模索する代わりに、Leanstralは腕をまくって取り組んだ。失敗した環境を再現するためのテストコードの構築に成功し、定義の等価性に関する根本的な問題を突き止めた。モデルは、defが明示的な展開（unfolding）を必要とする厳格な定義を作成するため、rwタクティックがマッチングに必要な内部構造を見るのを邪魔している、と正しく判断したんだ。

参考までに、Lean 4の論文： https://dl.acm.org/doi/10.1007/978-3-030-79876-5_37 (https://dl.acm.org/doi/10.1007/978-3-030-79876-5_37)

嬉しい驚きだ。「オープンソース」と言いつつ、本当にオープンソースであることを意味している人がいるなんて。重みはApache-2.0ライセンスみたいだね。

これ、数週間前にまさに予言してたよ。正しかったことが証明されて気分がいい！

LLMやそれに類する将来のツールの時代にどうなるか興味がある。将来のフェーズチェンジは、人間にとってのコードの書きやすさを無視して、証明可能性やテスト、そしておそらくトークン効率に焦点を当てるようになるんじゃないかと睨んでいる。

おそらくLeanとRustを組み合わせて、コンパイラに非常に適した形に凝縮したものになるだろう。高レベル言語で必要なものを指定すると、「バイブ・コーディング」の結果が返ってくる代わりに、正しさが証明されたコードが返ってくる。なぜなら、それだけがコンパイルに成功する唯一のコードだからだ。

https://news.ycombinator.com/item?id=47192116 (https://news.ycombinator.com/item?id=47192116)

最近、モデルのアライメントは相対的なものであり、アライメントの多様性が重要だという議論が盛んに行われている。Jack Clark（Anthropicの共同創設者）とEzra Kleinの最近のポッドキャストのエピソードを見てみてほしい。

ここでの多くのコメントが、Mistralのモデルが他の最先端モデルに追いついていないと指摘しているし、僕個人の経験も同じだ。でも、モデルのアライメント手法やそれをトレーニングする企業にはもっと多様性が必要だ。だから、この分野に真剣に取り組んでいる企業はどこであっても価値があるんだよ。

5,000ドルのハードウェアで自動定理証明器が動くというのは、未来のクールな姿だね。

HaikuとSonnetのpass@2はどうなってるの？