つぶやき: 数学の種類って１つじゃない

受験対策数学ばかりの定式化、定形化ばかりやってると、自由数学の解釈が読めなくなる。というのが、何となく解った。私の話が解らない理由に。

だから #Lean 形式化で、先にロジカル的に示す。その表現言語は後まわし。
私の言葉より先に #Lean4 の #形式化 されたコードを信用して欲しい。

私を否定するのは一向に構わない。

定理証明支援系言語の Lean を否定しても良い。だが Lean を否定する。
ならば、その不当性を示し、ダメ出しをすること。もちろん、私のコードの不当性を示してくれるのが、一番ありがたい。デバッグに協力してくれてありがとう。攻めを優先し、穴を見つける暇のある人は、手伝ってください。

なんなら、コードから各自の解釈で読み直す。言語化し直してもらいたい。
同じコンピュータで動く #OS を作ってる。#Windows / #Linux みたいな。

宇宙なんとか理論 が理解できず読めない。というのもそんな感じだったり？
もっと深くのところや別の概念、視点で、一般数学を超えないと？

自由数学をもっともっと経験してから読まないと、読解できないのだろう。

と、感じた瞬間があった。私の数学も誰にも理解できない理由にもなって…

私が一般数学を知らない…😅
Windows の内部をしらない。けど Linux 内部は解る。という意味になる。

けど、見ている「像」は同じもののはず…。言語が違う。OS が違う。
PC は規格通り同じもの。どちらの OS も動く。

#ZFC というものだ。クラシック数学者ならこの略称を知っているだろう。

ようするに、自分の数学を１から組み立てていくのが一番わかり易い。
習った数学を、自分数学に書き換えて覚えていくのが良いのかも。

2026/03/21 1:41

D.

#数学
#OS #Windows #Linux
#自分数学

Appendix

音楽に例えると

学校で習う「数学」は、音楽で言うところのクラシック音楽。
ちょっと、そこから別解を通して、同じ証明をするのが Jazz。

全く新しい、楽器を使って演奏するモダン数学。
音楽理論を無視して音を鳴らして遊ぶ自由数学。

みたいな感じであろう。

どの音楽をやっても「音」は出る。
感じ方が変わるだけだ。

空気を振動させ耳から脳🧠に伝える「音」🎵という本質は変わらない。

学校の数学をマスターすれば

まず、次に同じクラシック数学を教えられる先生となる。
別解で教える Jazz 数学な先生。

新しい楽器で現代数学を発明する数学者
「音」が鳴る事をパフォーマンスとして遊ぶ自由数学者

数学をマスターしなくても

本質の「音」は誰でも出せる。
つまり「数学」知識は不要。

その「音」が面白いか、ありきたりか、ちょっと変わっているか、
新しい感覚であるか？

そんな違い。

「音は誰にでも出せる」
数学とは無縁。

これに尽きる。

クラシック数学ばかりの数学者が多い気がする。
そう感じたって話である。

クラシックはクラシックの良さがある。が、その枠の中だけで良いのか？
自分に問うて、どんな数学音楽がやりたいのか？考えてみると良いかも。

「数学」は一つの概念では収まらない。✍️

#音楽
#数学音楽

リポジトリ DkMath

気長に #Mathlib を自分数学の #DkMath → #DkMathlib に置き換えていく
人生終末までの暇つぶしプロジェクト。

最終的には

import DkMathlib

として Mathlib をインポートしないで完全独立、切り離せるまでやり続ける終わらない数学プロジェクト。

https://github.com/Deskuma/dkmath

ああ。あほだよ。昔からそれは自覚している。言われなくとも知ってる。