Loading article…
Lean is a proof assistant and a functionalprogramming language.[2] It is based on the calculus of constructions with inductive types. It is a free and open-source software project hosted on GitHub. Development is currently supported by the nonprofit Lean Focused Research Organization (FRO).
Lean was developed primarily by Brazilian computer scientist Leonardo de Moura while employed by Microsoft Research and now Amazon Web Services and has had significant contributions from other coauthors and collaborators during its history.
Launched in 2013,[3] initial versions of the language, later known as Lean 1 and 2, were experimental and contained features such as support for homotopy type theory-based foundations that were later dropped.
Lean 3 (first released Jan 20, 2017) was the first moderately stable version of Lean. It was implemented primarily in C++ with some features written in Lean itself. After version 3.4.2, Lean 3 was officially end-of-lifed while development of Lean 4 began. In this interim period members of the Lean community developed and released unofficial versions up to 3.51.1.
In 2021, Lean 4 was released, which was a reimplementation of the Lean theorem prover capable of producing C code which is then compiled, enabling the development of efficient domain-specific automation.[4] Lean 4 also contains a hygienic macro system and improved type class synthesis and memory management procedures over the previous version.[5] Another benefit compared to Lean 3 is the ability to avoid touching C++ code in order to modify the frontend and other key parts of the core system, as they are now all implemented in Lean and available to the end user to be overridden as needed.[2]
Lean 4 is not backwards-compatible with Lean 3.[6] It uses the C++17 version of C++.[2]
In 2023, the Lean FRO was formed, with the goals of improving the language's scalability and usability, and implementing proof automation.[7]
2025年、ACM SIGPLANプログラミング言語ソフトウェア賞は、Gabriel Ebner、Soonho Kong、Leo de Moura、Sebastian UllrichのLeanに授与され、「数学、ハードウェアおよびソフトウェア検証、AIに大きな影響」を与えたことが評価されました。[ 8 ]
2026年、mathlibライブラリはオープンサイエンスに対するデマイリー賞を受賞しました。[ 9 ]
Leanには、依存型、型クラス、マルチスレッド、表現力豊かなタクティクス言語、モジュールシステムなど、関数型プログラミングや定理証明に役立つ多くの機能が含まれています。 [ 10 ]
Leanの公式標準ライブラリはStdと呼ばれ、ツリーマップ、ハッシュマップ、日時関数、並行処理プリミティブなど、プログラミングに役立つ一般的なデータ構造と関数が含まれています。[ 11 ]標準ライブラリは、コミュニティがメンテナンスしているバッテリーによって補完されており、数学研究と従来型のソフトウェア開発の両方に使用できる追加のデータ構造を実装しています。[ 12 ]
2017年に、研究レベルの数学まで、可能な限り多くの純粋数学を1つの大規模でまとまりのあるライブラリにデジタル化することを目標とした、コミュニティが維持するLeanライブラリmathlibの開発プロジェクトが開始されました。 [ 13 ] [ 14 ] 2025年5月現在、mathlibは21万を超える定理と10万を超える定義をLeanで形式化しています。[ 15 ]
その他のライブラリには、理論計算機科学ライブラリであるCSLib [ 16 ] 、 Leanでの科学計算用ライブラリであるSciLean [ 17 ] 、Leanを使用して物理学をデジタル化することを目標とするPhysLib [ 18 ]などがあります。
Leanは Visual Studio Code 、Neovim 、Emacsと統合されています。[ 19 ] インターフェースはクライアント拡張機能と言語サーバープロトコルサーバーを介して行われます。これらのエディタでは、UnicodeシンボルはLaTeXのようなシーケンスを使用して入力できます。たとえば、「×」などです。\times
自然数は帰納型として定義できる。この定義はペアノ公理に基づいており、すべての自然数はゼロであるか、他の自然数の次の数であるかのいずれかであると述べている。
帰納的Nat :型|ゼロ: Nat |拡張: Nat → Nat自然数の加算は、パターンマッチングを用いて再帰的に定義することができる。
def Nat.add : Nat → Nat → Nat | n , Nat.zero => n -- n + 0 = n | n , Nat.succ m = > Nat.succ ( Nat.add n m ) -- n + succ ( m ) = succ(n + m )これは簡単な証明です2つの命題PとQについて（接続詞と戦術モードを使用したリーンにおける意味合い：
定理and_swap ( p q : Prop ) : p ∧ q → q ∧ p := by intro h -- 証明 h で p ∧ q を仮定し、目標は q ∧ p であるapply And . intro -- 目標は 2 つのサブゴールに分割され、1 つは q で、もう 1 つは p · exact h . right -- 最初のサブゴールは、h : p ∧ q · exactの右側の部分と完全に一致するh . left -- 2 番目のサブゴールは、h : p ∧ q の左側の部分と完全に一致する同じ証明を項モードで示すと次のようになります。
定理and_swap ( p q : Prop ) : p ∧ q → q ∧ p := fun ⟨ hp , hq ⟩ => ⟨ hq , hp ⟩この定理は、SMTソルバーの手法を用いて証明を自動的に構築するグラインド戦術を用いて証明することもできる。
定理and_swap ( p q : Prop ) : p ∧ q → q ∧ p := by grindLean は、 Thomas Hales [ 20 ]、Kevin Buzzard [ 21 ] 、 Terence Tao [ 22 ] 、Heather Macbeth [ 23 ]などの数学者から注目を集めています。Hales は、自身のプロジェクト Formal Abstracts [ 24 ]に Lean を使用しています。Buzzard は、Xena プロジェクト[ 25 ]に Lean を使用しています。Xenaプロジェクトの目標の 1 つは、インペリアル カレッジ ロンドンの学部数学カリキュラムにあるすべての定理と証明を Lean で書き直すことです。Taoは、数学テキストの選択されたセクションの形式化からなる、実解析の教科書Analysis Iの Lean 版をリリースしました。[ 26 ] Macbeth は、学生に数学的証明の基礎を即時フィードバックで教えるために Lean を使用しています。[ 27 ]
2021年、研究者チームはリーンを使用して、凝縮数学の分野におけるピーター・ショルツェの証明の正しさを検証しました。このプロジェクトは、数学研究の最先端にある結果を形式化したことで注目を集めました。[ 28 ] 2023年、テレンス・タオはリーンを使用して、多項式フライマン・ルザ（PFR）予想の証明を形式化しました。この結果は、タオと共同研究者によって同年発表されました。[ 29 ] 2026年、エルデシュ問題728、[ 30 ] 347、[ 31 ]および369 [ 32 ]がAIの支援を使用して解決され、リーンで形式的に検証されました。
Physlib [ 33 ]は、数学における Mathlib と同様に、Lean における物理学の決定版ライブラリとなることを目指しています。物理学の基本的な定義、定理、計算を含む包括的なリポジトリとなることを目指しています。 インペリアル・カレッジ・ロンドンのKevin Buzzard氏は[ 34 ] 、形式化は数学に大きな影響を与えており、理論物理学も同様に扱われない理由はないと述べています。
「理想的には、100万行の物理演算データが必要ですが、それを実現するのは容易ではないかもしれません。もし機械が初期段階で物理演算をうまく処理できない場合は、最初は手作業が必要になりますが、最終的には機械がその役割を引き継いでくれることを期待しています。」
2025年、ジョセフ・トゥービー・スミスはLeanを使用して、2006年に発表された2ヒッグス二重項モデル（2HDM）ポテンシャルの安定性に関する 論文[ 35 ]の誤り[ 34 ]を発見した。
2022年、OpenAIとMeta AIはそれぞれ独立して、リーン環境で様々な高校レベルのオリンピック問題の証明を生成するAIモデルを作成した。[ 36 ] Meta AIのモデルはリーン環境で一般公開されている。[ 37 ]
2023年、ヴラド・テネフとチューダー・アヒムは、リーンコードを生成および検証することでAIの幻覚を減らすことを目指すスタートアップ企業Harmonicを共同設立した。 [ 38 ]
2024年、Google DeepMindはAlphaProof [ 39 ]を開発しました。これは、国際数学オリンピックの銀メダリストレベルのLeanで数学的命題を証明するものです。これは、数学オリンピックの問題でメダルに値するパフォーマンスを達成した最初のAIシステムでした。[ 40 ]
2025年4月、DeepSeekは、 DeepSeek-V3をベースに構築された、Lean 4での定理証明用に設計されたAIモデルであるDeepSeek-Prover-V2を発表しました。[ 41 ]
{{cite web}}: CS1メンテナンス: アーカイブサービスは非推奨になりました (リンク){{cite web}}: CS1メンテナンス: アーカイブサービスは非推奨になりました (リンク){{cite web}}: CS1メンテナンス: アーカイブサービスは非推奨になりました (リンク){{cite web}}: CS1メンテナンス: アーカイブサービスは非推奨になりました (リンク){{cite news}}: CS1メンテナンス: アーカイブサービスは非推奨になりました (リンク){{cite news}}: CS1メンテナンス: アーカイブサービスは非推奨になりました (リンク){{cite web}}: CS1メンテナンス: アーカイブサービスは非推奨になりました (リンク)