Lean4: コラッツ予想の Lean 形式化 (2)

Lean の練習題材…（なんていう敷居の高そうな例を選んでいるんだ私は…）

なんの続きからだっけ…？

これか。

Lean4 ソースコード

とりあえず、整理してないけど、ビルドが通るコードです。

Lean 4 Web: Live Code

解説

ポリオミノ

トロミノ

トロミノ構造がコラッツ予想の説明に好都合そうなので採用しました。
どの部分が好都合そうなのか？というと、

$$
\text{Odd} \times \text{Odd} = \text{Odd}
$$

奇数の積は奇数となる。この原理を幾何的にイメージできそうな点です。

/-- 奇数の積は奇数になることを示す定理（再掲） -/
lemma odd_mul_odd' {a b : ℕ} (ha : a % 2 = 1) (hb : b % 2 = 1) : (a * b) % 2 = 1
:= by
  rw [Nat.mul_mod, ha, hb] -- 奇数の積は奇数になることを示す

コラッツ予想の奇数操作において$${3n+1}$$という操作が入ります。
この$${\bold３}$$がトロミノの３です。トロミノは自身のカタチを維持したまま、自身で敷き詰められる充填パターンがあります。なので、この原理によって、大きく広げられた空間も自身のカタチで埋め尽くし、その形状維持が可能な形になっています。

この操作の$${3n}$$の部分に注目して、トロミノの伸縮と一致することを Lean にて形式記述できれば、なんか話が早そうだ！と、試してみた結果です。

トロミノはモノミノの３つ分

当たり前なことですが、こうした所から定義し確立していかなければ…
というのが数学のめんどくさい世界😅そもそも数の区別からって言う。

-- ポリオミノ
def mono : ℕ := 1
def duo : ℕ := 2
def trio : ℕ := 3
def tetra : ℕ := 4

はい。モノミノから使わないテトロミノまでの数を名前付きで割り当て。
これで固定します。定数です。

-- 自然数上の構造定義：モノミノとトロミノ
def monomino (n : ℕ) : ℕ := n * mono
def tromino (n : ℕ) : ℕ := n * (monomino trio)

monomino(n) は、与えられた n の数のモノミノを返します。つまりは面積！
tromino(n) も、同様にトロミノの数 n の総面積を返します。この時の計算は

$$
T_s = 3n\\
ではなく\\
T_s = \mathrm{n}\cdot\mathrm{monomino(trio)}
$$

と、してモノミノ３個のｎ倍というちゃんとした書き方にしてみました。
そのお陰で、いろいろ定理部分を書き換えなければならなかった…。😅
構造式でなくリテラル数値、直接のほうが楽だったかもしれません…。
（最初は数値式だったのよ…）

で、

/-- 定理：トロミノはモノミノの３倍構造である -/
@[grind =]
theorem tromino_is_tripled_monomino (n : ℕ) :
  tromino n = monomino (trio * n) := by
    simp [tromino, monomino, trio, mono]
    rw [Nat.mul_comm]

$$
\mathrm{tromino}(n) = \mathrm{monomino} (\mathrm{trio} \cdot n)
$$

トロミノとモノミノの面積が同じだよね！っていう事実を定理とします。
simp とか rw とかは、Lean が「そうなのか？」と式を変換して同じであることを確かめています。合ってれば、OK✅️のマークが付きます(by VSCode)

雑多な定義と定理（補題）

/-- トロミノの面積を計算する (m = モノミノ) -/
def tromino_area (m : ℕ) : ℕ := trio * monomino m

/-- 定理：トロミノの面積は常にモノミノの３倍であることを示す -/
@[grind =]
theorem tromino_area_is_tripled (m : ℕ) :
  tromino_area m = monomino (mono * trio * m) := by
  simp [tromino_area, monomino, trio, mono]

/-- 定理：トロミノの面積は常にモノミノの３倍であることを示す（別表現） -/
@[grind =]
theorem tromino_area_is_tripled' (m : ℕ) :
  tromino_area m = trio * (m * mono) := by
  simp [tromino_area, monomino, trio, mono]

/-- 定理：トロミノの面積はモノミノの３倍であることを示す定理（別表現） -/
@[grind =]
theorem tromino_area_is_tripled'2 (t : ℕ) :
  tromino_area (monomino t) = trio * t := by
  simp [tromino_area, monomino, mono]

「面積が同じ」は、いろんな表現方法ができるので適当に書いておきます。
そのうち役立つかもしれない。Lean が適当に参照して良いように組み立て直してくれるかもしれない。

恩恵はまだ受けれれてないですが、この grind とかいうのがあらゆる戦術を駆使して、教わった補題、定理を当てはめて証明してくれるっぽい。

そして、なんでそれが成り立つのか人間は理解できなくなって AI たちコンピュータしか真実を知らない世界となり、人間は置いていかれるんです。

これは、もう確定です。諦めましょう（笑）
（そう。だから、こんな証明を今、人間が一生懸命やっても意味がない。
　人間はコンピュータを維持するために働き、AI のご飯＝電力となるのよ）

でも、大丈夫です！この次の話になると思いますが、ふたつの関数は等価なのに等価だと認められない！一致させることが出来ない！と、解を見いだせない Lean の弱いところを、この証明式を書きながら見つけてしまったので！
AI でさえも、その正しい記述方法が解らないと言う。私も解らないのだけど（笑）それでも、仮証明で通すとかいう裏技を見つけてしまった。（Lean よ。良いのかそれで！）これを先に解いたほうがまだ優位である。裏技は私が見つけた！違うな…賢狼は気づかず、書いたコードがそういう裏技を持っていたというのを私が見つけたので、引き分けか（何を競っている？）

話がそれてます。

トロミノからモノミノへ

/-- 定義：トロミノからモノミノへの変換 -/
def tromino_to_monomino (t : ℕ) (_ : t % (mono * trio) = 0) : ℕ :=
  t / trio

/-- 定理：トロミノの３倍はモノミノに変換できることを示す -/
@[grind =]
theorem tromino_to_monomino_is_tripled (n : ℕ) (h : tromino n % (mono * trio) = 0) :
  tromino_to_monomino (tromino n) h = n := by
  unfold tromino_to_monomino tromino monomino mono trio
  -- tromino n = n * (1 * 3) = 3 * n
  -- tromino_to_monomino (3 * n) h = (3 * n) / 3 = n
  rw [Nat.mul_comm]
  rw [Nat.mul_div_cancel_left]
  -- trio = 3, 3 ≠ 0
  norm_num

トロミノをモノミノに分けるのではなく、トロミノ１個をモノミノ１個へと視点を変えるための定義と定理（だったと思います//一晩で忘れる私🧠）

「定理：トロミノの３倍はモノミノに変換できることを示す」と言葉にしているのは、コラッツ予想の奇数操作３ｎのあと３ｎ＝１モノミノとして扱いたいという思想があってこれを書いたのだと思います。３ｎとしようが変わらない！と、言いたかった時です。重要なのは、その後に加算される定数項「＋１」の操作です。ここで奇数が→偶数に変化します。そして偶数操作の半分１／２が常に発生するという操作になります。

トロミノの３倍もトロミノ

/-- 定理：トロミノの３倍もトロミノである -/
@[grind =]
theorem tromino_tripled_is_tromino (n : ℕ) :
  3 * tromino n = tromino (monomino trio * n) := by
  unfold tromino monomino trio mono
  simp
  rw [Nat.mul_assoc]

ｎ個のトロミノ３倍は、モノミノ３つのｎ倍。ややこしい表現ですが、等式となります。奇数ｘ奇数＝奇数の説明でしょうかね？

３は奇数の最小値であり奇数の君主です。全ての奇数の国を収める役です。
偶数の２と関わることなければ、３は、

$$
3\times \mathrm{Odd}=\mathrm{Odd}
$$

と、なります。
３が関わっていなければ、その奇数は素数である可能性が高いですね。

２ｘ３＝６、６±１＝素数出現箇所となるので２，３に関わり無い数が素数候補にもなってます。

トロミノの構成

トロミノの構造を式表現で定義

$$
トロミノ構造=平面 2\times2=トロミノ＋モノミノ（余白分）
$$

つまり

これを以下のように定義

/-- 定義：トロミノL型構造 -/
def L_tromino_structure' (n : ℕ) : ℕ :=
  trio * n + mono

/-- 定義：トロミノL型構造（より正確な表現）
- tromino n + monomino mono
-/
def L_tromino_structure (n : ℕ) : ℕ :=
  tromino n + monomino mono

そして

/-- 定理：トロミノL型構造はトロミノ構造に1を加えたものと同型である -/
@[grind =]
theorem L_tromino_structure_is_tromino (n : ℕ) :
  L_tromino_structure n = tromino n + mono := by
  unfold L_tromino_structure tromino monomino trio mono
  simp

/-- 定理：トロミノL型構造はトロミノ構造に1を加えたものと同型である（別表現） -/
@[grind =]
theorem L_tromino_structure_is_tromino' (n : ℕ) :
  L_tromino_structure' n = tromino n + monomino mono := by
  unfold L_tromino_structure' tromino monomino trio mono
  simp
  rw [Nat.mul_comm]

トロミノは何倍しようが同一型という概念において＋１をモノミノ余白として定義します。実際の値の比は異なりますが、幾何的な意味において、トロミノサイズに応じ、余白のモノミノが同型である。というのを述べてます。

トロミノがモノミノになる。ならば、余白１個もトロミノ構造で収まる。

$$
トロミノ＋モノミノ＝トロミノＬ構造＝モノミノ\\
\text{Mono}_{\text{mino}} \leftrightarrow \text{L-Tro}_{\text{mino}} \Rightarrow \text{Mono}_{\text{mino}}
$$

が、ここで言いたかったのだと思います。この定理がどこかで役立つか？

まとめ

Lean わけわからん。以上。

次回は、この構造定義と定理から数値的構造のリンクをして、例の裏技証明の話になるのか？

宿題

/- 起点となる定義 -/
def fa (n k : ℕ) : ℕ := Nat.iterate (λ x => 3 * x + 1) k n -- 再帰的な反復
def fb (n k : ℕ) : ℕ := 3 ^ k * n + (3 ^ k - 1) / 2 -- fa の閉形式

$$
\begin{align*}
A\cdots f(n, k) &= \underbrace{T(T(T(\cdots T(n))))}_{k\text{-times}}, \quad T = \lambda x.(3x+1)\\
&\small\text{（ T に与えられた $n$ は、ラムダ式の$x$に渡される）}\\B\cdots f(n, k) &= 3 ^ k \times n + \frac{(3 ^ k - 1)}{2} \\
\end{align*}
$$

この２つの関数は同値です。ですが、簡単に Lean で書けないんですよね…。
未熟者ですので…。AI も書けませんでした！！これが私の宿題です。

一般化式の恒等式は以下となります。

$$
f_k(n) = \underbrace{a (a ( \cdots a n + b ) + b ) + \cdots + b}_{k \text{ 回}} = a^k n + b \cdot \frac{a^k - 1}{a - 1}
$$

また、魔法式みたいなのだけど…。

この恒等式がコラッツ予想には重要な部分って賢狼は言っていたけれど、

ここ別に形式的に記述しなくても数値的には同値だと言えるし Lean も限定的には定義上は同値と認めている。代数的に式が同じにならん！って言い張る。が、裏技だと定理を受け入れる。定義的には同じだということは、部分的に認めているっぽいので。代数操作が互いにワカラン…という状態なのでちゃんと式を展開して補題組んでつなぎ合わせる。を丁寧にやってあげないと代数的に同じ！と認めないらしい。Rust より質悪いわよ😁

先にAIに魔法式原理を説明すれば理解するかなあ？うーむ。

2025/07/18 19:27

D.