Lean4: LEAN は将来 AI が使う言語

AI でも苦戦

プログラミングは小学生の頃からず～っとやってるので何の抵抗もないのだけど、これは、想像以上のパズルゲームだった！抜け穴が少ない…😅そりゃ
あったら逆に大問題となる。ゆえに。

バージョン問題

バージョンが異なるとライブラリ構成が異なってしまい AI が混乱しまくる
バージョン固定しとかないと話が噛み合わない。コーディング特化の AI が最適解を導き出すのに有効のようです。AI にも固定概念があり、一度これで通ると思ったコードを別の角度からのコードに置き換えるアイデアがなく、同じコードを何度も提案してきて堂々巡りに。創造の限界（というか AI は想像できない）ので、そこは人が逆にアシストしてあげる必要があります。

将来は、仕様が FIX され AI もバージョン混在の差異を考えなくて済むようになるでしょう。今は、この差異問題が難関で最適解を導くのが大変な言語となってます。しばらく安定するまでは混乱は続くでしょう。

コンパイルに時間がかかる

clean, build は、頻繁に行えない（笑）コア数の多い環境向け。

型の厳密性

Rust 以上に頑固です。
完全なロジックで証明とする。だから、仕方のない仕様です。
骨が何本も折れます。慣れなのでしょうが…。これからの世代は AI とともに考えながら組む言語ですね。そのうち、言語がエラーとともに、提案をしてくるのでしょう。

サンプル

サンプルとして完成した一部を例に。

以下の式のような結果を返したい

$$
\text{arctan}(y, x) =
\begin{cases}
\arctan(y/x) & \text{if } x > 0 \\
\arctan(y/x) + \pi & \text{if } x < 0 \text{ and } y \geq 0 \\
\arctan(y/x) - \pi & \text{if } x < 0 \text{ and } y < 0 \\
\pi/2 & \text{if } x = 0 \text{ and } y > 0 \\
-\pi/2 & \text{if } x = 0 \text{ and } y < 0 \\
0 & \text{otherwise}
\end{cases}
$$

は、こうなります。

def floatPi : Float := 3.141592653589793

def floatAtan (y x : Float) : Float :=
  if x > 0.0 then
    Float.atan (y / x)
  else if x < 0.0 ∧ y ≥ 0.0 then
    Float.atan (y / x) + floatPi
  else if x < 0.0 ∧ y < 0.0 then
    Float.atan (y / x) - floatPi
  else if x == 0.0 ∧ y > 0.0 then
    floatPi / 2.0
  else if x == 0.0 ∧ y < 0.0 then
    -floatPi / 2.0
  else
    0.0

$${π}$$ など定数が用意されているのですが、型が異なると全く使えない様になってます。自動で型変換はされません。昇格させるには明示します。

ライブラリに無い定数は、上記のように自分で定義して利用します。
演算できない式も式のまま評価されます。そんな感じの証明言語です。

Unicode で特殊な数学記号も、ソースコード中に記述していきます。

成果物

structure ComplexF where
  re : Float
  im : Float
deriving Repr

instance : Add (ComplexF) where
  add a b := ⟨a.re + b.re, a.im + b.im⟩

def expF (z : ComplexF) : ComplexF :=
  let r := Float.exp z.re
  ⟨r * Float.cos z.im, r * Float.sin z.im⟩

def zetaVectorF (n : Nat) (t : Float) : ComplexF :=
  if n = 0 then ⟨0.0, 0.0⟩ else
    let n_sqrt := Float.sqrt (Float.ofNat n)
    let logn := Float.log (Float.ofNat n)
    let θ := -t * logn
    let z := ⟨0.0, θ⟩
    let e := expF z
    ⟨(1.0 / n_sqrt) * e.re, (1.0 / n_sqrt) * e.im⟩

def partialZetaSumF (N : Nat) (t : Float) : ComplexF :=
  (List.range N).map (λ n => zetaVectorF (n + 1) t) |>.foldl (· + ·) ⟨0.0, 0.0⟩

notation "ℂ" => Complex Float

def zetaRe (σ t : Float) (bound : Nat := 1000) : Float :=
  List.foldl (λ a b => a + b) 0.0 $
    List.map (λ n =>
      let x := Float.ofNat (n + 1)
      Float.cos (t * Float.log x) / Float.pow x σ) (List.range bound)

def zetaIm (σ t : Float) (bound : Nat := 1000) : Float :=
  List.foldl (λ a b => a + b) 0.0 $
    List.map (λ n =>
      let x := Float.ofNat (n + 1)
      Float.sin (t * Float.log x) / Float.pow x σ) (List.range bound)

-- zetaRe σ t bound + i * zetaIm σ t bound
def zetaComplex (σ t : Float) (bound : Nat := 1000) : ComplexF :=
  { re := zetaRe σ t bound, im := - (zetaIm σ t bound) }

たったこれだけのコードに、４～５時間かかってしまった（笑）

2025/04/10  6:25

D.