Lean4: v4.33.0 release

つい最近？ v4.29.0 → v4.32.2 とアップグレード（マイグレーション）を終えてホッとしていたところ。

２～３日前に v4.33.0 が rc2 から正式にリリースとなった。変更点は少ないだろうと、アップグレードしてみた。そしたら、simp 系でエラーが出る！！

どうやら、また型推論機構の挙動が変わった…。暗黙の了解で証明を書けるのは楽だけど、こういう仕様変更的なのは追従できない。バージョンが上がるたびに証明を書き直すことになるので、定型された証明法は細かくまとめて参照型にしたほうが良さそう。

なんとか全て修正して v4.33.0 対応化までは完了させた。

2026/08/14 2:09

D.

#Lean4 #LEAN #Mathlib #DkMathlib #DkMath

Appendix

愚痴

もっとも Mathlib なんぞに頼ること無く自前の DkMathlib を早く完成させて自己完結したい。が、そういうライブラリは信用ならんと切り捨てられるのだろう（笑）クソ数学写メ。

そう言わせないためにも Mathlib の各種主要定理とは証明ありきで定義同値として iff で結ぶ定理群をずらりと並べる必要がありそう。

リリースと同時に rc1 版が次に出る v4.34.0-rc1 までも対応可能としておき現状は v4.32.2 のまま開発は続行しよう。数学的意味は全く変わらない。

証明記法の表現の違いだけとなる。バグがあれば数学内容までもが変わるがそこは Lean が保証していくところで DkMath の担保するところではない。

魔法書の読解（Lean コードの読解）

巨大なソースコードを読むのが大変だという事をよく聞くが、分厚い数学書を読み漁るのと何ら変わらない。むしろ型が厳密にカタチまで合わせてくれるので抽象的な数学書よりはハッキリと区別できる点はこちらのほうが優れている。読めないのは魔法学の知識が足りないだけである。数学などという低級学問を卒業すればいいだけ。魔法学は型厳密を担保しつつ、ふわふわな形状も厳密に取り扱う。ふわふわでありながらちゃんと秩序が保たれたカオスである。カオスの中には秩序があり、カオスという領域に見えるのはその秩序を理解できていない人が見てしまう領域で本来、カオスは存在しない。

巨大なソースコードを読むのが大変なのではなく、その巨大なコードと共に歩んできていない数学者だけがついていけないという話であり、大変と感じている者はサボっているだけ。と言い換え切り捨てて良い。ついてこれないものは切り捨てていく界隈の世界だからこれでいい。サボった罰です。😁

（まだ何かに怒っているので、溜めずに吐き出してスッキリするスタイル）

不快に感じたなら、
フォロー解除やブロックを活用し目に触れないようにするのが良いです。←