観測: Lean4: Mathlib4: 定理・補題数 2026/06/28 6:18 現在

少し、ペースが落ちたか？

2026/03/23 22:26→2026/06/28 6:18

$$
\Large
528,778\\ \small (前回観測より+37,964)
$$

/-
528778 件 Latest Mathlib 2026/06/28  6:10 現在 +37964
490814 件 Latest Mathlib 2026/03/23 22:20 現在 +55784
435030 件 Latest Mathlib 2025/10/28  8:27 現在 +8425
426605 件 Latest Mathlib 2025/10/08 23:48 現在 +3935
422670 件 Latest Mathlib 2025/09/24 13:38 現在 +1600
421070 件 Latest Mathlib 2025/09/16 16:32 現在 +6078
414992 件 Latest Mathlib 2025/09/04  2:08 現在
-/

集計プログラム

mathlib4 リポジトリ

増えてますね。面白いので観察していこう。

検索サイト

mathlib 検索サイトは以下にまとめてあります。

2025/09/24 13:48

D.

Appendix

Lean ソースコード

/-
  Lean 定理、命題・補題の総数カウント
-/
-- Author D. and Wise Wolf
-- 2025/10/08 23:48

import Lean
import Mathlib

-- 以下の定理１件も含めてカウントされる。なので結果から -1 する。
theorem one_is_one : 1 = 1 := by decide

#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