Lean: Version 4.27.0 release

前回、書いたのは２つ前の 4.25.0 だった。
4.26.0 すっ飛ばして
4.27.0 今日、リリースです (2026/01/24)

Lean

リリースノート

cid: 6974283f-0c4c-8323-9316-fe7613925635

主要項目の解説

うむ、Lean 4.27.0（2026-01-24）のリリースノートじゃな。
この版は 372個の変更が入っており、機能追加・修正だけでなく、性能改善と“開発者体験”の底上げが目立つ回じゃ。

以下、「何が嬉しいか／どこが壊れやすいか」を中心に、噛み砕いて解説するぞい。

1. 目玉（Highlights）

✅ Module System が “実験卒業”

これまで `experimental.module` によって扱われていた 新モジュール機構が安定版扱いになり、`experimental.module` オプションは no-op（実質無効）になった。
→ つまり「もう常用してよい」扱いじゃな。

✅ backward.* は“引っ越し用の仮橋”

`backward.*` 系の互換オプションは 短期の移行補助で、導入から 6か月後には予告なく消える可能性がある、と明記された。
→ 依存してるなら早めに脱出経路を作るのが吉。

✅ 速度とメモリが気持ちよくなる

• Language Server（特に watchdog）のメモリが減り、Mathlibで約1GB削減という強めの改善。

• import 時のファイルシステムアクセス最適化で Linuxで~3%高速化（環境次第で増える）。

✅ エラーメッセージの“人間化”

エラーに ヒント・提案・説明リンクが増える方向の改善がまとめて入っておる。
→ Lean初心者だけでなく、古参も「何が起きてる？」が早くなるタイプ。

2. `grind` がさらに強くなった（特に関数の等式）

4.27 は grind強化回と言ってよい。

✅ 関数値の合同閉包 `funCC`（デフォルトON）

部分適用された関数同士の等式をちゃんと追跡するようになり、

• `f a = a` から `(f a) m = a m`

• `f a = g` から `f a b = g b`

みたいな推論が自然に通る。

✅ `grind_pattern` に guard が入り、暴発を抑えられる

定理インスタンス化を「条件が揃った時だけ」に絞れるようになって、探索爆発が減る。

✅ `grind` が BitVec / lia / ring に拡張

`grind ring` / `grind lia` が `BitVec` を扱えるようになった。

3. 破壊的変更（ここだけ注意じゃ）

🔥 String API：部分文字列が `String.Slice` に統一

`String.drop` / `String.take` などが `String.Slice` を返す方向に整理され、これまで `String` が返っていたコードが落ちることがある。

典型的な修正：

• `f (s.drop 1)` が通らない → `f (s.drop 1).copy`

• 比較も `s.drop 1 == "Hello".toSlice` のように Slice 前提へ

これは「遅くなる」ではなく、むしろ コピー削減で速くなる方向の設計じゃ（必要な時だけ `.copy`）。

🔥 Iterator API：`Std.Iterators` → `Std` に移動

`Iter` や `IterM` などの定数が `Std` 直下へ。壊れたらまず

open Std

を試すのが早い。

🔥 `noConfusion` が hetero に一般化

手で `noConfusion` を直に使ってる場合に破壊が起きうる（`rfl` を渡す・`eq_of_heq` を挟む等が必要）。

4. 言語・コンパイラ・ツール周りの改善

✅ well-founded recursion（特に `Nat` 測度）が“計算できる”方向へ

通常、well-founded recursion は reducible にしにくいが、測度が `Nat` の場合は燃料で構造再帰に落とせて reduce できるようになり、`@[semireducible]` も警告なしで受理される。
→ `by decide` が通る範囲が増えるタイプのありがたさじゃ。

✅ Compiler：パッケージ間のシンボル衝突を回避

異なる Lean パッケージ由来の（非 `@[export]`）定義の衝突を防ぐ修正など。

✅ Language Server：メモリ削減＋補助機能の改善

未知識別子の quick-fix が module 内で `public/meta` を正しく挿す等。

✅ Lake：モジュールが複数パッケージにある時の解決

「同名モジュールが複数パッケージに存在」みたいな状況を Lake が解決する手続き追加。
また build target での package 名に workspace-index を入れるなど、運用上の衝突を避ける方向。

✅ `shake`（Mathlib系運用）にフラグと注釈が増強

import を“どこまで残すか”をより精密に制御できるようになった（keep-implied/keep-public 等、注釈 `-- shake: ...`）。

5. いちばん実務的な「移行チェックリスト」

１．String 系が落ちたら：`String.Slice` を疑い、必要箇所に `.copy`
２．Iterators が見つからない：`open Std`
３．`noConfusion` を手で叩いてる：hetero 化の影響を確認
４．`backward.*` 依存：半年後に消える前提で撤去計画
５．`grind` を使う証明：`funCC` と `grind_pattern guard` の恩恵を受けに行く

この 4.27.0 は、わっち的に言うと
「巨大都市（Mathlib）で暮らすための道路整備・治安改善・交通最適化」が一気に進んだ回じゃな。

Lean で研究（特にお主のように理論を積む者）をやるなら、`grind` 強化と `Nat` well-founded 周りの reducible 改善は、地味に効いてくるはずじゃ。

👩‍⚕️ せっかく通ったビルドが、通らなくなることがないよう願うのみ…ｗ

2026/01/24 11:11

D.

#Lean 4.27.0, 4.26.0 #release #リリース #リリースノート

Appendix

ちなみに…。

Version 4.26.0

うむ、Lean 4.26.0（2025-12-13）の主要点を「何が嬉しいか／何に注意か」だけ拾って解説するぞい。
（この版は 264件の変更が入っておる）

1. Lake：依存パッケージを “セマンティックバージョン範囲” で指定できる

Lake で Reservoir 依存を `^1.2.3` みたいな semver 範囲で要求できるようになった。
`lake update` 時に、範囲を満たす最新版を選んでくれる。

2. `grind` 大強化回（制御・診断・対話が一気に良くなった）

✅ `grind_pattern` 制約（暴走インスタンス生成を止める）

定理のインスタンス化が無限に増殖しがちなケースを、
`grind_pattern ... where ...` で 生成条件を縛って止血できる。

✅ `#grind_lint`（危険な `[grind]` 定理を診断）

`@[grind]` を付けた定理が E-matching で爆発するかを検査するコマンドが入った。

✅ 対話モードの機能増加（finish?/cases_next/have ? など）

`finish?` の生成スクリプトがより扱いやすくなり、
`cases_next` や `have x? : P`（grindで自動証明して状態観測）が追加。

✅ さらに：`grind?` の基盤も更新

`grind?` が “`grind => finish?`” の新基盤で動くようになった。

3. `try?` が拡張できる（ユーザー拡張ポイント追加）

`try?` に ユーザー定義の提案エンジンを差し込めるようになった。
`@[try_suggestion]` か `register_try?_tactic` で提案を追加できる。

4. マッチコンパイルが速く・賢くなった（大きい `match` が改善）

大きい `match` のコンパイルが最適化され、
不要な分岐を避けたり、疎なケース分析（sparse）を使ったりする改善が入った。
互換のために `backwards.match.rowMajor` で旧挙動へ戻せる。

5. ライブラリ：日常が地味に楽になる更新たち

代表的なのだけ挙げると…

• リストのスライス記法 `xs[1...5]` が入った

• 文字列まわりの整備：`String.Slice.replace` など、Slice基盤の強化

• Iterator：`Iter.size` が `Iter.count` に置き換え（`IteratorSize` は非推奨へ）

• `String.ofList` / `String.toList` を推奨ルートにして、旧APIを整理

6. ⚠️ 破壊的変更：FFI に大ダメージ（BaseIOが “ゼロコスト化”）

`BaseIO` が `IO.RealWorld` パラメータを消してゼロコスト化された。
これは FFI にとって大きな破壊と明記されておる。

7. Server / Lake の品質アップ（大事故を減らす系）

• Server ログが LSP メソッドでフィルタできるように改修

• Lake のテンプレートが「今の toolchain に対応する Mathlib」を使うよう調整

• Lake の module build key が package でスコープされ、別パッケージで同名モジュールを扱いやすくなった

4.26.0 を一言で言うと

この版は 「grind の制御性・診断性を上げて、Lake の依存管理を semver 化し、内部はBaseIOゼロコストで軽くした」回じゃ。

お主のように Lean を研究基盤として使うなら、
4.26 = “自動化（grind/try?）と運用（Lake）の土台が強くなった”と見てよいぞい。