LEANってなに？

LEANと聞いて、パッと何かわかる方はほとんどいらっしゃらないかと思います。
LEANとは数学の形式化と形式検証のために構築された関数型プログラミング言語で、定理証明支援システムです。
こういった定理証明支援システムは他にもいくつかあります。coqの方がメジャーですかね。
これらのシステムの目的は、証明が正しいことを保証することです。
まぁ細かい前置きは置いておいて、大学以来に久しぶりに触りたいなぁと思ったので、触っていきたいと思います。

LEANのインストール

VS Codeに拡張機能が用意されています。
他にも利用する方法はありますが、これが公式の推奨ですし、個人的にも一番楽でおすすめです。

LEANのチュートリアル

さっそく触っていきましょう！
今回は久しぶりなので、チュートリアル「Natural Number Game」をやってきます。
（自分がやってた頃はこんなものなかったぞ。。）

左の説明を読むと、まずは「2 + 2 = 4」が成り立つことを証明してみるようです。
そのあとに、「x + y = y + x」が成り立つことを証明し、最後は「フェルマーの最終定理」を証明できるか確認してみるそうです！
わくわくしてきますね！

フェルマーの最終定理とは、「nが3以上の自然数のとき、x^n+y^n=z^nを満たす自然数(x,y,z)は存在しない」というもので、数学が好きな人なら一度は聞いたことがある超有名かつ人気定理です！

さて、「Tutorial World」をクリックして始めてくださいとあるのでクリックします。
左の説明が変わりました、「Start」をクリックします。

「37x + q = 37x + q」を証明します！
LEANでは「Tactics（戦術）」を用いて、定理を証明します。最初に使うのはrflという戦術です。
これは「X = X」を証明する戦術のようです。
画面右側のTacticsのrflをクリックすると説明が表示されます。

入力欄にrflと入力して実行します！
ちなみに右上のコマンドラインのボタンを押すとコードを書けるのでそっちの方がオススメです！

こんな感じでガンガンやっていきます！
ネタばれになるので、この記事ではここまでにします。

特殊文字の入力方法

LEANでは数学で使うような特殊文字を多用します。
たとえば、自然数の集合を表す「ℕ」や、実数の集合を表す「ℝ」などです。
VS CodeのLEAN拡張機能には、これらの特殊文字を簡単に入力する方法が用意されています。
よく使うものを紹介しておきます。

記号	入力方法	説明
ℕ	\N	自然数の集合
ℝ	\R	実数の集合
→	->	左ならば右
←	<-	右ならば左
↔	<->	左右両方ならば
∀	\forall	全称記号
¬	\not	否定記号
∨	\or	OR
∧	\and	AND
∈	\in	要素である

他にもたくさんありますが、よく使うものはこんな感じです。

まとめ

久しぶりに触ったら思ったより覚えてなさ過ぎて、試行錯誤しながらチュートリアルをやってみてます（笑）
こういうマイナーで公式のドキュメントくらいしか調べようがないものは嫌でも試行錯誤するので、一昔前のコーディング（生成AIが流行る前）を思い出せて楽しいですね！
ご興味がある方は是非触ってみてください！

弊社では一緒に働く仲間を募集中です！

現在、様々な職種を募集しております。
カジュアル面談も可能ですので、ご連絡お待ちしております！

募集内容等詳細は、是非採用サイトをご確認ください。