LEAN

実用日本語表現辞典

lean

別表記：リーン

「lean」の意味

「lean」という単語は、主に2つの意味を持っている。一つ目は、物や人が「痩せている」または「脂肪が少ない」という意味である。例えば、痩せた人や低脂肪の食品を指す場合に使われる。二つ目は、物体が「傾く」または「もたれる」という意味である。例えば、壁に寄りかかっている人や傾いた建物を指す場合に使われる。

「lean」の発音・読み方

「lean」の発音は、IPA表記では /liːn/ となる。IPAのカタカナ読みでは「リーン」となり、日本人が発音するカタカナ英語では「リーン」と読む。発音によって意味や品詞が変わる単語ではないため、どの場合でも同じ発音である。

「lean」の定義を英語で解説

英語での「lean」の定義は、"(of a person or animal) thin, especially healthily so; having no superfluous fat." または "be in or move into a sloping position." である。前者は「人や動物が痩せていて、特に健康的に脂肪がない状態」を意味し、後者は「傾いた状態にあるか、傾く動作をすること」を意味する。

「lean」の類語

「lean」の類語としては、痩せている意味では「slim」、「thin」、「slender」などが挙げられる。傾く意味では「tilt」、「slant」、「incline」などが挙げられる。これらの類語も同様の意味で使用されるが、ニュアンスや強さが異なる場合がある。

「lean」に関連する用語・表現

「lean」に関連する用語や表現としては、「lean on」、「lean against」、「lean towards」などがある。「lean on」は「もたれかかる」、「lean against」は「～に寄りかかる」、「lean towards」は「～に傾く」といった意味で使われる。

「lean」の例文

1. He has a lean body.（彼は痩せた体をしている。）
2. The company is trying to become more lean and efficient.（その会社はより痩せて効率的になろうとしている。）
3. The tower is leaning to the left.（その塔は左に傾いている。）
4. She leaned against the wall to rest.（彼女は壁に寄りかかって休んだ。）
5. The tree is leaning towards the house.（その木は家に向かって傾いている。）
6. The meat is lean and healthy.（その肉は脂肪が少なく健康的だ。）
7. The athlete has a lean physique.（その選手は痩せた体格をしている。）
8. The fence is leaning due to the strong wind.（強風のためにフェンスが傾いている。）
9. The cat leaned on the warm radiator.（猫は暖かいラジエーターにもたれかかった。）
10. She leaned towards the idea of studying abroad.（彼女は留学する考えに傾いていた。）

（2023年6月7日更新）

デジタル大辞泉

リーン【lean】

読み方：りーん

［形動］《やせた、引き締まった、などの意》生産方式や企業で、無駄を排したさま。「力強い―な会社」

三国志小事典

楽安Le an

	ラクアン	県
【県長】韓当 【県人】

楽安国Le an

	ラクアン	領城9 戸数74,400 人口424,075
【郡王】劉建 / 劉伉 / 劉寵 / 劉鴻 【王相】魯恭 / 李尤 【太守】崔篆 / 劉嘉 / 薛漢 / 李章 / 陸逢 / 陸康 / 陳蕃 / 何夔 / 管統 / 楊沛 / 夏侯恵 / 桓嘉 / / / 管統 / 楊沛 / 何夔 / 夏侯恵 【郡吏】何寵 【郡人】任嘏 / 任燠 / 周宣 / 孫歴 / 孫旂 【領城】臨済 / 千乗 / 高菀 / 楽安 / 博昌 / 蓼城 / 利 / 益 / 寿光

外国人名読み方字典

Lean

名前 リーン； レアン

ウィキペディア

Lean (証明アシスタント)

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2026/08/23 21:58 UTC 版)

Lean

Leanのロゴ
パラダイム	関数型プログラミング
登場時期	2013年 (2013)
開発者	Leonardo de Moura Lean FRO
最新リリース	v4.33.0/ 2026年8月10日 (2026-08-10)
型付け	推論される, 強い, 静的
影響を受けた言語	ML Coq Haskell Prolog Rust Scheme
影響を与えた言語	koka
プラットフォーム	クロスプラットフォーム
ライセンス	Apache License 2.0
ウェブサイト	lean-lang.org

Cantorの定理をLeanで示している様子。右側の infoview に今使える仮定と示すべきゴールが常に表示される。

Lean（リーン）は、定理証明支援系、および関数型プログラミング言語である。数学の定理やプログラムの性質や仕様を形式的に記述し、それらについての証明をコンピュータで検査するために用いられる。主にレオナルド・デ・モウラによって開発が始められ、現在は Lean Focused Research Organization とコミュニティによって開発されている。

概要

純粋関数型言語として

プログラミング言語としての Lean は、純粋関数型言語である。この点では Haskell と似ているが、Haskell とは異なる点として以下が挙げられる。

• Lean は依存型を持つ。
• Haskell は遅延評価であるが、Lean は正格評価である。
• Lean の do 構文はより柔軟で、for / while ループや break / continue が自然に表現できる。
• Lean は Functional but in-place と呼ばれる参照カウントに基づく最適化を行う。

マクロを持つ言語として

また、プログラミング言語としての Lean は、真のマクロを持つ拡張性の高い言語でもある。この特徴は Common Lisp、Rust、Julia 等と似ているが、これらの言語とは異なる点として以下が挙げられる。

• まず Common Lisp と比較すると、Lean のマクロは 衛生的(hygienic) である。これは、マクロ処理の過程で識別子の名前が衝突しないことを意味する。
• Rust や Julia と比較すると、Lean のマクロは「言語に最初から搭載されていたかのように」ユーザ定義の構文やコマンドを追加できるという点が異なる。Rust のマクロは macro! という形でなければならず、Julia のマクロは @macro という形でなければならないが、Lean のマクロにそのような制約はない。

定理証明支援系として

Lean は定理証明支援系でもあるが、その基盤は依存型にある。依存型があるということは、カリー・ハワード同型対応によって「高階述語論理を型として表現できる」ということを意味する。これにより、Lean は数学の証明をプログラムとして表現できる。これは他の依存型に基づく定理証明支援系（Rocq や Agda や Idris）と同様である。また、逆に言えば同じく定理証明支援系である Isabelle とは Lean は理論的基盤が異なる。

「依存型に基づく定理証明支援系」の中でも、Lean は以下の特徴によって他と区別される。

• Agda や Idris とは異なり、Lean にはタクティクフレームワークが存在し、対話的な定理証明と自動証明を強力にサポートしている。
• Rocq は Lean と同様 CIC(Calculus of Inductive Constructions) をベースにしており型システムは似ているが、Lean はメタプログラミングフレームワークがより強力である他、Rocq は Lean のように汎用言語としてはデザインされていない。

プログラム検証器として

Lean はプログラミング言語でもあるため「Lean で書いたプログラムを Lean で検証する」ことが可能であり、これに命令的コードが書けることを併せると「命令的なコードを Lean で書いて Lean で検証する」ことが可能である。これは Dafny を想起させる性質だが、Dafny は de Bruijn 基準を満たしていない、つまり「独立に検査可能な証明項を生成しない」ため Lean に比べて信頼性が低いという違いがある。

歴史

2013年: 開発開始

Lean はGitHubでホストされているオープンソースプロジェクトである。2013年にMicrosoft Researchのレオナルド・デ・モウラによって立ち上げられた。

Lean の開発時点で Coq や Agda など他の定理証明支援系は存在しており、Lean の言語仕様はそれらから大きく逸脱したものではなかったが、新しい証明支援系を考案した理由として、次の2点がある。

• 証明のホワイトボックス自動化ツールを開発するためのプラットフォームを作成すること- Z3 SMT ソルバの開発者でもある Leonardo de Moura は、標準的な SMT 実装の長所と同時に限界も認識していた。特に SMT ソルバの設定を変更することができず、フリーサイズ(one-size-fits-all)な設計となっていることは、ブラックボックス的な性格を持つとされた。ホワイトボックスアプローチとは、ここではSMTソルバを構成する要素をユーザが必要に応じて組み替えたり再構成したりできるように公開することを指す。対話的定理証明支援系(interactive theorem prover、 ITP)のタクティク言語は、ホワイトボックス化を実現する手段として位置づけられ、オーダーメイドの自動化を段階的に開発できるものとされた。これは SMT と対話的定理証明の間のギャップを埋めることを目的としていた。
• 小さな型理論とカーネル - Lean という名前には、英語で「痩せている」とか「贅肉がない」という意味がある。Lean の基礎としては標準的な依存型理論(dependent type theory)を最小限の理論に圧縮したものが採用されているが、これが Lean という名前の由来である。Lean では、タクティクを発展・洗練させる一方で、タクティクの出力を検証するシステムの実装を可能な限り単純に保つことが設計方針とされた。Lean の設計方針は、依存型理論の他の実装と比較して「より複雑な論理を、より単純なシステムで表現する」ことにあると説明されている。Lean が影響を受けかつ最も Lean に近い型理論を採用している Coq と比較すると、Lean は fixpoint 演算子や型システムに埋め込まれたモジュールシステムがないなどの違いがある。

2014年: Lean 0.1

最初のプロトタイプは Lean 0.1 (2014 年) である。Lean 0.1 では ML ライクな構文が導入され、それは後のすべての Lean のバージョンで継承されることになる。単純な simp タクティクが既にこのバージョンから存在した。帰納型のサポートはまだなく、手で公理(axiom)を追加する必要があった。Lean 0.1 では、Lua スクリプトによる構文と戦術の拡張がサポートされていたが、この部分は後の Lean 3 で削除されることになる。

2015年: Lean 2

2015 年、Lean の最初の公式リリースである Lean 2 が発表された。帰納型の適切なサポートや組み込みタクティクの拡張など、欠けていた重要な機能が追加されたほか、主要な機能として Lean 2 ではホモトピー型理論 (HoTT) のサポートが追加された。

2017年: Lean 3

最初にリリースされた比較的安定したバージョンは Lean 3 で、2017年の1月20日にリリースされた。Lean 3 では、あまり使用されていなかった Lua による構文拡張機能が削除され、根本的に異なるアプローチが採用された。Lean 自体がプログラミング言語とされ、Lean 自体によりタクティクの定義やそのほかのメタプログラミングが可能になった。Lean 2 からのもう一つの大きな変更は、ホモトピー型理論 (HoTT) のサポートの廃止である。HoTT のサポートが廃止された理由としては、

• 証明無関係(proof irrelevance) の公理がないと、タクティクを効率的に実装するのが難しくなり、コードの重複が生じるという問題
• 当時 「book HoTT」と最近の計算的な Cubical Type Theory のどちらが望ましいか不明だったという問題

が挙げられる。また、Lean で数学を形式化するライブラリである mathlib がコミュニティ管理の 独立したプロジェクトとして分離された。

バージョン3.4.2以降、Lean 3の開発は正式に終了し、Lean 4の開発が始まった。

2021年: Lean 4

2021年、Lean 4の最初のマイルストーンリリースが発表された。C++ではなく Lean 自身によって再実装され、定理証明支援系であると同時に汎用プログラミング言語でもあるという位置づけが強められた。

Lean 4 より以前のバージョンでは、次のような問題点が認識されており、Lean 4 ではそれらへの対応が行われた。

• Lean 3 での経験から、定理証明を実用的に行うためにはメタプログラミングフレームワークを備え、高い拡張性を備えていることが重要だとわかっていた。しかし Lean 3 のシステムの多くの部分が、C++ で書かれた Lean 3 のソースコードを変更しない限り、ユーザには変更できなかった。
• Lean 3 メタプログラミングは仮想マシン解釈のオーバーヘッドにより非効率だった。これにより Lean 3 での自動証明は、C++ や OCaml のような効率的なコンパイラを持つ言語で実装された同様の自動証明とは競合できなかった。

Lean 4 は完全に拡張可能であり、パーサ、エラボレータ、タクティク、決定手続き(decision procedure)、プリティプリンタ、コードジェネレータを変更・拡張することができる。また Lean 4 は対話的証明のためにカスタマイズされた衛生的なマクロ(hygienic macro)を持つ。Lean の構文をユーザが改変する際に C++ コードに触れる必要はなくなった。

さらに Lean 4 ではメモリ管理手続きが改善されたほか、テーブル解決に基づく新しい型クラス解決アルゴリズムが使用され、パフォーマンスが改善された。また、Lean 4 は functional but in-place と呼ばれる新しいプログラミングパラダイムに基づくようになった。

Lean 4 には Lean 3 との後方互換性はない。Lean3 で開発されていた主要なライブラリとして、2017年ごろから開発が行われていたmathlib が挙げられるが、コミュニティにより Lean4 への書き直しが行われた。これには100万行以上のコードを書き換える必要があったが、この移行作業は2023年7月に完了した。

2023年: Lean FRO設立

2023年7月、Lean Focused Research Organization (FRO) が設立された。形式数学の発展に向けて、証明のUI改善、スケーラビリティの改善、証明の自動化といった問題に取り組むとしている。また2023年9月、最初のLean 4 の公式リリースが発表された。

Leanの型システム

無矛盾性

非形式的な数学において一般的に基礎理論として採用されているのは ZFC 集合論と呼ばれる理論であるが、Lean で採用されている基礎理論は Calculus of Inductive Constructions (省略して CIC と呼ばれる) であって、これとは異なる。

Lean の型システムの無矛盾性については、Lean 3 の時代の結果として、「 ${\\displaystyle ZFC_{\\omega }}$

Lean の構文の例

Lean はオブジェクト指向言語ではないとされている。しかし、関数適用を「まるでフィールドにアクセスするかのように」書くことができる記法が用意されている。これは Nim 言語における Uniform Function Call Syntax に似ている。

structure Point (α : Type) : Type where
  x : α
  y : α

-- アクセサ
#check (Point.x : {α : Type} → (Point α) → α)
#check (Point.y : {α : Type} → (Point α) → α)

def origin : Point Int := { x := 0, y := 0 }

-- 通常の関数適用の書き方
#guard Point.x origin = 0

-- フィールド記法。`.x` を付けるだけで値にアクセスできる
#guard origin.x = 0

テーブル化型クラス解決(Tabled Typeclass Resolution)

Lean 4 の型クラス解決アルゴリズムは、実行時間を指数的に改善した。

型クラスは、プログラミングと定理証明の両方において、アドホック多相性 を実現する仕組みである。しかし、数学ライブラリ Mathlib の中で型クラスが広く使われるにつれ、既存の型クラス解決手続きの理論的限界が問題となった。既存の型クラス解決手続きの主要な理論的限界とは、次のようなものである：

• ダイアモンドが存在する場合、指数関数的に実行時間が伸びてしまう
• サイクルが存在する場合に発散が生じる

Lean 4 では、この２つの問題を解決する新しいアルゴリズムであるテーブル化型クラス解決が実装されている。このアルゴリズムは Prolog に対して1998年に 提案された型クラス解決アルゴリズムに基づく。

モナドとモナド変換子

Lean は Haskell の影響を受けており、モナドとモナド変換子が標準ライブラリに深く組み込まれている。

純粋関数型言語において手続き的な計算をエミュレートする方法としてはモナドの他にも代数的エフェクト・ハンドラが知られている。代数的エフェクト・ハンドラはモナドに比べると、たとえばモナドを入れ子にしたときにモナドをリフトするような操作が必要ないという利点がある。

代数的エフェクトについては Lean の開発者たちによって検討されたことがあるが、実行時またはコンパイル時のオーバーヘッドが避けられずパフォーマンス上の懸念があるという理由で採用されなかったという経緯がある。

拡張された do 記法

Lean は純粋関数型言語であるため、手続き型言語では暗黙に扱われる副作用を、モナドという再利用可能な抽象的要素で再定義することで扱っている。この再定義によって、副作用をより厳密に制御したり、派生的な副作用を導入したりすることを可能にしている。モナドは Haskell で広く用いられる抽象化機能であり、その糖衣構文である do 記法と結びついている。

Lean では、メタプログラミングフレームワークを用いて、Haskell の do 記法に由来する構文が拡張されている。具体的には以下のような記法を最初からサポートしている。

• 可変な変数を let mut で宣言できるようにする Rust ライクな記法
• 早期リターン(early return)
• for ループ、break や continue といった制御フロー

たとえば、以下は Lean 4 で実装したエラトステネスの篩である。

/-- `n`以下の素数のリストを `Array Bool` の形で返す。
`i` 番目が `true` ならば `i` は素数で、`false` ならば合成数。 -/
def eratosthenesAux (n : Nat) : Array Bool := Id.run do
  let mut isPrime := Array.replicate (n + 1) true

  isPrime := isPrime.set! 0 false
  isPrime := isPrime.set! 1 false

  for p in [2 : n + 1] do
    if not isPrime[p]! then
      continue

    if p ^ 2 > n then
      break

    -- `p` の倍数を消していく
    let mut q := p * p
    while q ≤ n do
      isPrime := isPrime.set! q false
      q := q + p

  return isPrime

/-- エラトステネスの篩 -/
def eratosthenes (n : Nat) : Array Nat :=
  eratosthenesAux n
  |>.zipIdx
  |>.filterMap fun ⟨isPrime, i⟩ =>
    if isPrime then some i else none

#guard eratosthenes 10 = #[2, 3, 5, 7]

#guard
  let actual := eratosthenes 100
  let expected := #[
    2, 3, 5, 7, 11,
    13, 17, 19, 23, 29,
    31, 37, 41, 43, 47,
    53, 59, 61, 67, 71,
    73, 79, 83, 89, 97
  ]
  expected == actual

Functional but in-place

Lean 4 のベンチマークにおける実行時間を Haskell、 OCaml、 Standard ML、 Swift と比較した表。

ほとんどの関数型言語は、メモリ管理を自動で行うためにガベージ・コレクタを利用している。一方で、各値の正確な参照カウントを保持することで、破壊的更新などの最適化が可能になる。Lean は、純粋な関数型言語でありながら参照カウントを利用してメモリ管理を行う。参照カウントがちょうど１の値（つまり共有されていない値）を更新するとき、自動的に破壊的更新が行われる。このことを指して、Lean のプログラミングパラダイムのことを functional but in-place (FBIP) と呼ぶ。特に、Lean で配列のようなデータ構造を扱うとき、FBIP によりコードの純粋性を保ちながら効率的なコードを生成することが可能である。これにより、Lean のコンパイラが生成するコードの効率化が図られている。

Lean が値の破壊的変更を行う例として、次のようなコードがある。

-- Lean のオブジェクトのメモリ上でのアドレスを取得する関数
-- 参照透過性を壊すため，unsafe である
#eval ptrAddrUnsafe #[1, 2, 3]

/-- フィボナッチ数列を計算する -/
def fibonacci (n : Nat) : Array Nat := Id.run do
  -- 可変な配列 `fib` を宣言している
  let mut fib : Array Nat := Array.mkEmpty n
  fib := fib.push 0
  fib := fib.push 1
  for i in [2:n] do
    -- ここで配列 `fib` のメモリアドレスを表示させている
    dbg_trace unsafe ptrAddrUnsafe fib
    fib := fib.push (fib[i-1]! + fib[i-2]!)
  return fib

-- 値がコピーされていれば異なるメモリアドレスが表示されるはずだが...?
#eval fibonacci 15

衛生的マクロとメタプログラミング

ITP（対話的定理証明支援系）において、構文を拡張可能にすることは、複雑な数学的対象の表現や、ライブラリ開発における再利用可能な抽象化に関わる。Lean 3 のものを含め、既存の ITP のマクロシステムには、構文拡張の抽象化や名前の衝突に関する課題があった。

問題点は主に以下の２点である：

• マクロの抽象化が弱く、しばしば冗長な定義をせざるをえなかった。
• タクティクを定義する際などに、マクロ展開において名前の偶発的な衝突が起こってバグを生み出していた。

Lean 4 では、Scheme ファミリーに着想を得た新しいマクロシステムが導入された。このマクロシステムは、複数のマクロ抽象化レベルを単一のシステムで扱い、表現力と名前の衝突回避を両立することを目的としている。

たとえば、以下は Coq のライブラリ math-comp における和のΣ記号の定義である。ここでは、少しずつ異なる同様の定義が 12 回繰り返されている。

Reserved Notation "\\sum_ i F"
  (at level 41, F at level 41, i at level 0,
           right associativity,
           format "'[' \\sum_ i '/  '  F ']'").
Reserved Notation "\\sum_ ( i <- r | P ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \\sum_ ( i  <-  r  |  P ) '/  '  F ']'").
Reserved Notation "\\sum_ ( i <- r ) F"
  (at level 41, F at level 41, i, r at level 50,
           format "'[' \\sum_ ( i  <-  r ) '/  '  F ']'").
Reserved Notation "\\sum_ ( m <= i < n | P ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \\sum_ ( m  <=  i  <  n  |  P ) '/  '  F ']'").
Reserved Notation "\\sum_ ( m <= i < n ) F"
  (at level 41, F at level 41, i, m, n at level 50,
           format "'[' \\sum_ ( m  <=  i  <  n ) '/  '  F ']'").
Reserved Notation "\\sum_ ( i | P ) F"
  (at level 41, F at level 41, i at level 50,
           format "'[' \\sum_ ( i  |  P ) '/  '  F ']'").
Reserved Notation "\\sum_ ( i : t | P ) F"
  (at level 41, F at level 41, i at level 50). (* only parsing *)
Reserved Notation "\\sum_ ( i : t ) F"
  (at level 41, F at level 41, i at level 50). (* only parsing *)
Reserved Notation "\\sum_ ( i < n | P ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \\sum_ ( i  <  n  |  P ) '/  '  F ']'").
Reserved Notation "\\sum_ ( i < n ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \\sum_ ( i  <  n ) '/  '  F ']'").
Reserved Notation "\\sum_ ( i 'in' A | P ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \\sum_ ( i  'in'  A  |  P ) '/  '  F ']'").
Reserved Notation "\\sum_ ( i 'in' A ) F"
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \\sum_ ( i  'in'  A ) '/  '  F ']'").

ほぼ同じことが Lean の数学ライブラリ mathlib4 では次のように表現されている。

syntax bigOpBinder := term:max ((" : " term) <|> binderPred)?

syntax bigOpBinderParenthesized := " (" bigOpBinder ")"

syntax bigOpBinderCollection := bigOpBinderParenthesized+

syntax bigOpBinders := bigOpBinderCollection <|> (ppSpace bigOpBinder)

syntax (name := bigsum) "∑ " bigOpBinders ("with " term)? ", " term:67 : term

これは Lean では syntax および declare_syntax_cat というコマンドが用意されていることと関係がある。Lean ではユーザが構文カテゴリを定義し、パーサの拡張を抽象化された高水準言語で行うことができる。これは Lean 3 までの静的なマクロでは不可能だった。

自動証明

定理証明支援系のコミュニティにおいて、自動証明は大きな関心事である。典型的なものに SMT ソルバーを使用して証明を自動化しようとする試みがある。有名な例として、Isabelle における Sledgehammer が挙げられる。Lean にも SMT ソルバーに影響を受けた自動証明タクティクである grind が存在する。

grind には以下のような特徴がある。

• grind の中核的な動作原理は合同閉包(congruence closure)であるが、補助定理を E-マッチングを用いてインスタンス化する機能を有しておりユーザが拡張可能である。

• grind は CIC の内部で直接動作し、検証可能な証明項を生成する。Isabelle の hammer が「証明目標を外部の論理体系へ変換して SMT ソルバーを呼び出して解く」のとは対照的である。
• grind は型クラスによってパラメトライズされた補助ソルバーを持ち、適切な代数的インターフェースを実装している任意の型に対して動作する。

利用

• 2020年12月、数学者の Peter Scholze は自身の liquid vector space に関する定理を Lean で形式化することは可能かという挑戦状を Lean コミュニティに持ち込んだ。この挑戦は Liquid Tensor Experiment と呼ばれ、2022年7月に完了が宣言された。
• 2022年2月、Open AI が国際数学オリンピック(IMO)級の数学問題の証明を Lean で生成するモデルを開発した。このモデルは miniF2F ベンチマークで 41.2% の正答率を達成した。
• 2022年11月、Meta AI も国際数学オリンピック級の数学問題の証明を Lean で生成するモデルを開発している。このモデルは miniF2F ベンチマークで 67% の正答率を達成した。
• 2024年、Google DeepMind は AlphaProof を開発した。AlphaProof も、国際数学オリンピック級の数学問題の証明を Lean で生成するモデルである。 AlphaProof は miniF2F ベンチマークにおいて 95% 以上の正答率を達成した。 AlphaProof と AlphaGeometry2 を組み合わせたシステムは、IMO でメダル相当の成績を達成した初の AI システムである。
• 2024年、AWS は Cedar 言語の正しさとセキュリティ特性を保証するのに Lean を使用した。
• 2025年、Harmonic の AI システムであるアリストテレス(Aristotle)が、IMO 2025 の 6 問中 5 問を解いた。これは IMO 金メダルに相当する成績である。Aristotle において Lean は最終的に答えを検証するときだけでなく、証明の探索時にも使用された。ただし、幾何問題だけは Lean ではない別の専用ソルバーが Lean の外で解いている。 なお、「IMO 金メダル相当の AI システム」としては Google Deep Mind の方が早い。
• 2026年1月、1975年に提起されて以来未解決だったエルデシュ問題728の証明がAIによって発見され、Lean で証明が形式化された。研究の主導者である Nat Sothanaphan は、この研究を「エルデシュ問題をAIシステムで自律的に解いた最初の例である」としている。
• 2026年3月31日、証明支援系Leanを用いて遠アーベル幾何学の主要定理を形式化し、さらに宇宙際タイヒミュラー理論を形式化し検証することを目的とするLANAプロジェクトがZEN大学より発表された。LANAは「Lean for ANAbelian geometry」の略称で、最初のLはLeanのLである。
• 2026年8月1日、OpenAIは自社のAIモデルAstraを使って数学と理論計算機科学にまたがる10件の未解決問題について新たな成果を上げたと発表した。各論証はLeanで形式化され検証可能な証明として記述された。形式化された証明データはGitHubで公開された。
• 2026年8月10日、Anthropicは未公開の研究版Claudeを用いてリーマン予想に関連する問題に成果を上げたことを発表した。結果はLeanを用いて形式化され、論文の主要な定理を機械的に検証できる形式で記述した証明がGitHubで公開された。

受賞歴

• ACM SIGPLAN Programming Languages Software Award (2025年)
  • 受賞理由として、Leanが数学、ハードウェアおよびソフトウェアの検証、そしてAIの分野に大きな影響を及ぼしていることが挙げられている。また、LeanはAIを用いた数学的推論システムにおける事実上の標準的な選択肢であると評価された。
• CADE Thoralf Skolem Award (2025年)
  • 2015年のCADE論文「The Lean Theorem Prover (System Description)」が受賞した。
  • 同賞は、発表から年月を経て分野に大きな影響を与えたことがわかったCADE論文に授与される賞である。
  • 「数学の形式化やソフトウェア検証をはじめとして、数多くの応用が生まれている」と評価された。
• Jean-Pierre Demailly Prize for Open Science in Mathematics (2026年)
  • 数学におけるオープンなプロジェクトを表彰する賞であり、Lean ではなくLean の主要な数学ライブラリである Mathlib が受賞した。
  • 「数学の実践そのものを長期的に変革し得る基盤」として評価された。

関連項目

• 型理論
• 依存型
• 関数型プログラミング
• Coq
• Agda
• Isabelle

外部リンク

• Lean Website Lean の公式サイト。
• Lean 4 Web Lean のオンラインエディタ。
• Reservoir Lean のパッケージレジストリ。パッケージをインデックスするだけでなく、ビルドとテストも行う。
• vscode-lean4 VS Code に Lean 言語のサポートを追加する拡張機能。Unicode 記号をサポートしていて、× に対する \\times のようなLaTeXに似たシーケンスを使用して入力ができるようにする。

Weblio日本語例文用例辞書

「Le an」の例文・使い方・用例・文例

• Conteeさんは、昨年Hope and Learnの会長に就任された、受賞歴のあるミュージカル女優さんです。
• Hope and Learnは遠隔地に学校を建設する資金を集める慈善団体です。
• Hope and Learnへの寄付は、この夜会の最後に集めます。
• 遅れないようにしよう では時に Let's don't be late. も用いられる》.
• (紀元前 43 年, Antony, Octavian, Lepidus /lépədəs/の)第 2 回三頭政治.
• ペニシリンV（商標名Ledercillin VK）の形
• Leontodon属の様々な一般的な野生の草花のどれでも
• Lepidobotryaceae科に属している双子葉植物の木の属
• 7はJanuaryseventhと読む
• 今年の1 月まで、「Premiumアイスクリーム」で知られるErnesto Dairyの副社長だったCarla Starkが、4 月20 日付けでHolman Health社の会長に就任することが今日発表された。
• Holman Healthは栄養補助食品業界の巨大企業で、最高経営責任者であるBud Rollinsを交代させようとしているが、Bud Rollinsは機会があるたびに、彼と同社取締役会とがあらゆる点で合意できるようには思えないと公言していた。
• Holman Healthの株主は、StarkがErnestoに行ったのと同じ魔法をかけてくれることを大いに期待していると報じられている。Starkは、Ernestoがグルメアイス市場において驚くべき20％というシェアを獲得することになった「Premiumアイスクリーム」のブランドを作り上げた人物である。
• Holman Healthを辞職し、政界入りをするつもりである。
• Holman Healthを辞職し、Ernesto Dairyに勤めるつもりである。
• Holman Healthで問題を抱えていた。
• 私はまず、この点をAmandaに確認します。
• 11月21日にHolyoke Bar and Grillで、Pete Laurenの退職パーティーが開かれることをお知らせします。11 月10 日までにお返事をください。
• 議事録を取ったのは書記Grace Tanaka。
• 来月のロンドンへの出張のために、飛行機の便を予約して、Southland銀行の近くの宿泊施設を手配してもらえますか。
• 面接を行う予定だった、営業部長のDon Richmanが、家庭の事情で突然呼び出されたことをお知らせするために、Eメールを差し上げています。