Solve a simple theorem using Lean4

-- Import necessary libraries for natural numbers
import Mathlib

-- Theorem: For any natural number n, n + 0 = n
theorem add_zero1 (n : ℕ) : n + 0 = n := by
  -- Proceed by induction on n
  induction n with
  | zero =>
    -- Base case: n = 0
    rfl  -- reflexivity: 0 + 0 = 0
  | succ n =>
    -- Inductive case: n = succ n
    rw [Nat.add_succ]  -- Rewrite (succ n + 0) as succ (n + 0)

ふと気が付いたのだが，ChatGPTは"Leanでの簡単な証明見せてくれ"というと，Lean3のコードを出してくる。Lean4でやってくれ，というと出してはくれるのだが，イマイチ精度が悪い。少なくともLean4のprojectを作ってあげないと，Mathlib4が正常に動作しない。
Coqではここまで苦労はしないはずなので，やはりマイナー言語なりの難しさがあるようだ。
この実験は，「生成AIを使って未知の言語をどこまで自力で学習できるか」の挑戦。今となってはPythonは，習熟度の差こそあれ，自習でも習得にそこまで苦労しない。これでは初学者の気持ちが分からない。Lean4ならば，自分はろくに内容を知らないので，初学者の気持ちになれる。
もしこのやり方で「生成AIを使うことの危うさ」が分かれば，それが次世代のプログラマの仕事になる。例えば「まずLean3のコードを出してしまう」などは，言語のversion違いの問題をプログラマが認識していないと対処できない恐れがある。