京都大学の望月新一教授が新たなブログを出し、 この中でLean4の素晴らしさについて語っていた。 今、彼の新理論は学術界において半ばトンチキとして認知されているが、 これは単に数学が高度化しすぎたために理解出来る人が少ないし 理解しようともしないクソ風土があるとして、 だったらLean4で証明してやんよ！とのことである。
とってもいい試みであると思う。 このことはニュースにもなっていた。
打開策として、望月氏が示しているのが、定理証明支援ソフト「Lean（リーン）」の活用だ。 Leanは、数学の証明の「正しさ」をコンピューターが判定するツールで、「証明チェッカー」とも呼ばれる。米マイクロソフトリサーチが開発した。証明を構成する定義や概念、論理の流れをすべてプログラムのコードとして記述し、コンピューターがその整合性を1行ずつ検証していく仕組みだ。 https://www.asahi.com/articles/ASTCY1BZVTCYDIFI00XM.html
おれが最近、ブログでLean4について注目していると書いたら、 突然、天才の望月新一氏がLean4について注目しだしたからびっくりした。 おれはまだ、ラムダノートから出ている「ゼロから始めるLean言語入門」という本を 途中までしかやっていないレベルなのでもちろん貢献出来るわけがないが、 Lean4という言語が数学の最先端を切り開く未来に対しては大いに期待している。 というかなぜそうならないのかが不思議でしょうがないレベルだ。
ところでこのLean4だが、実はBlueskyで知らない人に突然教えてもらった。 無職で暇なので、関数型言語でまともに開発出来るようになってみようかなとつぶやいてたら、 おそらく京大卒の謎の人物から、「Haskellなんかもうオワコンなので今からならLean4が良い」 と言われて、Lean4について調べるに至った。
おれはこういうことがとても多い。 例として他にも、おれは学部時代の研究テーマが木構造の可視化技法（ツリーマップとかが有名）だったのだが、これはコードを書いてみればわかるが、ツリーマップであれば木構造の葉に対してなんらかの数値を 計算する必要がある。例えば、株などのデータであれば株価の統合的な情報から、 評価額などを抽出する必要がある。おれは当時、関数型については1ミリも知らなかったが、このようなmap的な操作がプログラミングでは有効だということに独自に気づき、概念をラッパーにより変換するという意味で「概念ラッピング」と呼んでいた。すると、情報学科のやはり謎の人物が現れて、「それはmapという操作だ。SICPという本を読んでみるといい」と言われて、関数型言語にたどり着いたというわけである。2010年頃のことである。 おれは度々こういうことが起きるが、Lean4の次は何だろうか。
そのLean4だが、おれは望月氏とは異なり、数学の証明器としてよりはむしろ、一般的なソフトウェア開発を厳密に行うためのツールとしてLean4に注目している。また、その厳密さが、チャッピーによるコーディング補助を前提としたソフトウェア開発に活きると考えていることはすでに話した。 実際、ブロックチェーンのCardanoでは、Lean4の応用が始まっているようである。
formal verification of Cardano smart contracts. Leveraging the Lean4 proof system and SMT solvers, it automatically checks that contracts behave as intended without requiring developers to write manual proofs. https://cardano.org/news/2025-07-17-a-new-era-of-smart-contract-verification/
現状でもRustなどを書いていると、コンパイラのサポートを出来るだけ活かせるようなコードをいかにして書くかが鍵となる感覚があるが、今後はより高度な証明がソフトウェアにつけられていき、より厳密でより正しいソフトウェアが開発されていく方向に進んでいくのだと思う。Lean4はその最有力言語と言ってもよいだろう。