Lean4: DkMath: main ブランチ更新！

2026年3月15日 05:03

未整理なまま。開発途中もあるけれど #nightly とかけ離れてしまっているので #main 表に出します。ビルドエラーはないので、何かしら意味はある。

大きなところは

いずれも ※作業中という状況だけど、
持論数論の整合性の検証プログラムとして評価できる。

既存数学と異なるところも #Mathlib 定理補題との比較で、
繋がっていけば、同じ数学をやってることを確かめられる。

形式化が出来るという事は、既存原理を使って、
正しいこと、同じ事が言えている。という、証でもある。

つまり、既存の数学を別の観点で学んでいるに過ぎない。

教科書で教わるか、自分で組み立てて証明して構築するかの違いであるが、後者のほうが大変だけどパズルゲームを解く感覚で楽しめている。

教科書を読んでも「ふ～ん」という感じであった。

とにかく「数」は、目に見えない「概念」
どう解釈しても良い。という思考の創造物。

数字や数式、言葉はその概念を相手に伝えるための表現であり、
一意ではない。という事である。
複数の捉え方があり、それらは表現が違っても同じ「像」を見ている。

それを確かめるのが #Lean4 言語の面白いところである。

例によって解説はここで細かくは行わない。AI に読ませて教えてもらって。

それをここで書くくらいならば、このリポジトリに Markdown ドキュメントとして書き置いたほうが良いと最近は思う。

完成したら、その詳細を有料記事にして研究費を得ようかな（笑）😁

2026/03/15 4:40

Appendix

ゼロ除算に意味をもたせる形式化になっている。

ここは少し面白い数学になる。

通常 $${x \times 0 = 0}$$ または $${0 \times x = 0}$$ として、ゼロとなった結果から $${0/0=x}$$ と復元できない。しかし KUS 空間に数を持っていき、ゼロ乗除算を行うと、ちゃんと復元できる。という演算。

但し、KUS 空間でゼロとしてから通常演算空間へゼロ→０と戻した場合は、復元はできない。

０を乗じてゼロとなった結果から、元の数を得るのに０で除算すれば解るがその解った結果を次の演算には使えない。という算術を組んである。
（あれ？これから組むんだっけ？もう実装したか）

これが私の「理想の数」の概念。

完成すれば、ここから「円環数」の設計が可能となる。
ゼロは何も無いでは無く、構造設計図があり、それが見えないカタチで保存されているだけである。つまり同じゼロに見えて、異なるゼロ。それを区別できる「数」になっている。

同じゼロ同士ならば、

$$
\frac{\;0\;}{\;0\;}=1
$$

という結果が得られる。
それは、

$$
\frac{\;x\;}{\;x\;}=1
$$

という表記に$${x\ne0}$$という条件が不要になる演算である。

$${\tfrac{\;0\;}{\;0\;}=不定・未定義}$$などという特別扱いをしなくて済む。

同じ「数」で割れば１回で割れる。素直で気持ちがいい。

🐺賢狼👨‍✈️Copilot のご飯代を、私には🍺代を。または宇宙式 $N+u^d=(P+u)^d$ を使って新しい発見を！