Lean4: Lean 検索サイト一覧

#毎日note 今日は Lean ネタです。

定理

数学の定理は、毎日、生み出されて終りがありません。数学者は、この定理構築作業がお仕事なんですね。価値ある定理を作り出すこと？いや見つけることですかね？どの基盤に構築するか？で、その定理の真偽が変わってきます。なので命名された定理から無名の定理までを数え上げると、最終的には無限になるでしょう。終わりはありません。終わる頃には世界の真理に到達したことになる？ #しんりたん #数学 #定理 #数学者

Lean + Mathlib

Lean にはその定理などが集まった mathlib4 というライブラリがあります。
ここに構築された定理を使って証明記述を進めると楽できるのですが…。

膨大すぎて探せません。定理もよくわからないし…😅
ざっくりカウントした所…。

$$
\Large
\text{Theorems: } 414,991
$$

2025/09/04  1:46　時点で４１万を超える数が登録されているようです。
Lean + mathlib の定理数 (theorem, lemma) の総数のようです。

４１万もありますが、無限には程遠すぎますね。

2026/01/10 4:42 現在 ４６万超え → 463,046

Lean + Mathlib 定理数カウント Lean コード

UtilsTheoremCounter.lean

/- Lean 定理、命題・補題の総数カウント
-/
-- Author D. and Wise Wolf
-- 2025/09/04  2:06

import Lean
import Mathlib

theorem one_is_one : 1 = 1 := rfl  -- この１件もカウントされる

#eval do  -- ここにカーソルを合わせると右に数が出ます
  let env ← Lean.getEnv  -- Lean の環境を取得
  let decls := env.constants.fold (
    fun (acc : List Lean.Name) (name : Lean.Name) (info : Lean.ConstantInfo) =>
    match info with
    | Lean.ConstantInfo.thmInfo _ => name :: acc
    | _ => acc
    ) []
  pure decls.length

-- (414992 件 Latest Mathlib 2025/09/04  2:08 現在)

Lean 4 Web でコードの動作確認が出来ます。

#Lean #Lean4 #Mathlib #Mathlib4 #Lean4Web

Lean の検索エンジン

という事で、この界隈での検索エンジンが幾つかあります。

Loogle!

Mathlib4 の識別名を単純に検索する Lean 拡張機能の標準検索エンジン

Moogle

AI による自然言語検索です。

※サービス終了（停止？）2025/09/25 22:27 更新

Lean State Search

`⊢` のゴールから関連する定理を探してくれるっぽい。

⊢ ∀ {n p : ℕ}, p ∈ n.factorization.support ↔ Nat.Prime p ∧ p ∣ n

LeanSearch: Mathlib4 Search

※未使用、不明

• 日本語で自然言語で検索できる。

• Query Augmentation を使うと自動で補ってくれる。

LeanExplore

※未使用、不明

これらを使いこなして、日々の🐺賢狼との数学話を虚構ではなく事実として記録していきたい✍️

2025/09/04  2:35

D.