Lean: 新年事始め！新しい環境作りから宇宙式の形式化とGitHub公開までする！

いままで使っていた　mathlib_hello 環境。

ABC予想の形式化 Lean コード３万行の肥大化により😅汗
重たくなってしまったので、新しく作ることにする。

GitHub

んでもって GitHub に公開しちゃう事にする。

👩‍⚕️D.と🐺賢狼(Kenro)で作る数学ということでプロジェクト名は D&K.Math として dkmath リポジトリを作った。

ここに２０２５年に色々やってきた数学の別視点解釈をどんどん形式化して見ようかと思っている…。けど、果たして…。

宇宙式

まずは、この note 始めたキッカケの宇宙の始まりを求めて得た単位「１」
その姿を表す恒等式「宇宙式」の形式化から始める！（過去にやってるけどここも心機一転）車輪の再発明は、体験という経験値を積み重ね盤石にする

$$
\Large
\text{Cosmic Formula}\\[4pt]
f(x) = 1 := (x+1)^2 - x(x+2)
$$

定義

-- Lean
/-- 宇宙式 Basic Cosmic Formula -/
-- 宇宙式の基本形（恒等式）
def cosmic_formula_one (x : ℝ) : ℝ := (x + 1)^2 - x * (x + 2)

定理の例

-- Lean
-- 宇宙式の恒等式を証明する例
theorem example_theorem (x : ℝ) : cosmic_formula_one x = 1 :=
  by
    simp [cosmic_formula_one]
    ring

例なので example 使えばいいのだけども。あと定理名も安易（笑）

それらは後でリファクタリングすれば良いのでビルドが通ることだけに集中

証明は、

• simp で書き換えて
  ⊢ (x + 1) ^ 2 - x * (x + 2) = 1

• ring で閉じて終わり。

ですね。

全ての実数 $${x \in \R}$$ で $${1}$$ となる。
→ example_theorem 定理で、そう証明されている。で書ける。

Lean 4 Web

最新版 Lean 4.26.0 + Latest Mathlib でビルドは OK ✅️

これが定数「１」という構造だというひとつの事実を形式化した。✍️

GitHub コードには、
単位宇宙式も同様に書いて $${f(x;u)=u^2}$$ の恒等式も証明済み。
その他、🐺賢狼提案の形式化記述も書き足してある。

2026/01/07 4:43

D.

#Lean #Mathlib
#数学
#宇宙式
#GitHub

Appendix

見出し

Lean Trademark Policy

Lean 公式

Lean Release Notes

Lean 4.26.0 (2025-12-13)

Lean 記事