実験ノート：lean4-skillsを試す、ベンチーマークの例題mathd_algebra_69を解いてみる。

背景：lean x codexのnoteを見た

Lean x codexで、Hilbertという、ゴールに対してLean記述を生成し、これを解けるまで自律的にtry&errorを行うというシステムにインスパイアされて、codexとプロンプトでこれを試してみた記事があった。

Hilbertの論文はこちら： https://arxiv.org/abs/2509.22819

codexでできるということは、Claude codeでもできるだろうか？

前の記事で、Claudeにlean4-skillsを導入し、COBOLの形式検証を行った。

Skillがあれば、codexと同様のことができるのでは？ということで実験。

お題はmathd_algebra_69

もとのnoteでは、miniF2Fという数学ベンチマーク の問題の１つである mathd_algebra_69を解かせていた。HuggingFaceにあるデータセットをみると。

theorem mathd_algebra_69
 (rows seats : ℕ)
 (h₀ : rows * seats = 450)
 (h₁ : (rows + 5) * (seats - 3) = 450) :
  rows = 25 := sorry

解説を読むと、

question.leanにお題をコピーし、windowsのフォルダに設置する。

VSCodeからlean4が立ち上がり、、infoViewが立ち上がる。

ダメダメである。

ClaudeでLean4 skillsをつかってみた

さて、Claude Desktopのcodeから、ローカルフォルダを指定して、解いてみる。

ファイルを読んで、それからSkillの /lean4:autoproveを今回は使う。

信じられん、autoproveが見つからなった？？？

何回か、「許可」のお伺いがきて、実行を続けると。。。証明ができたという。

そして、指定したフォルダのquestion.leanは、書き換わって、sorry以下が実体化されていた。

import Mathlib.Tactic

theorem mathd_algebra_69
 (rows seats : ℕ)
 (h₀ : rows * seats = 450)
 (h₁ : (rows + 5) * (seats - 3) = 450) :
  rows = 25 := by
  have hseats : 3 < seats := by
    by_contra h; push_neg at h
    interval_cases seats <;> omega
  zify [show 3 ≤ seats from le_of_lt hseats] at h₀ h₁
  nlinarith [sq_nonneg ((rows : ℤ) - 25), h₀, h₁, Int.natCast_nonneg rows]

VSCodeで開くと、Mathlibがインポートされないというエラーがでた。これはインストールが大変なようなので、今回はパス。

ChatGPT（無料）にも聞いてみた。

ということで、29秒の推論で、以下の証明を提示してきた。

import Mathlib.Tactic

theorem mathd_algebra_69
 (rows seats : ℕ)
 (h₀ : rows * seats = 450)
 (h₁ : (rows + 5) * (seats - 3) = 450) :
  rows = 25 := by
  -- 自然数の等式を整数に持ち上げる
  have h0 : (rows : Int) * (seats : Int) = 450 := by norm_cast; exact h₀
  have h1 : (rows + 5 : Int) * (seats - 3 : Int) = 450 := by norm_cast; exact h₁

  -- (rows+5)*(seats-3) - rows*seats = 5*seats - 3*rows - 15 を得る
  have diff : (rows + 5 : Int) * (seats - 3 : Int) - (rows : Int) * (seats : Int)
              = 5 * (seats : Int) - 3 * (rows : Int) - 15 := by ring
  -- h1 と h0 を使って 5*seats - 3*rows - 15 = 0、すなわち 5*seats - 3*rows = 15
  have linear : 5 * (seats : Int) - 3 * (rows : Int) = 15 := by
    calc
      5 * (seats : Int) - 3 * (rows : Int)
        = (5 * (seats : Int) - 3 * (rows : Int) - 15) + 15 := by ring
      _ = 0 + 15 := by rw [←diff, h1, h0]; simp
      _ = 15 := by simp

  -- linear を rows で掛けてから h0 を代入して多項式を得る
  have mul_rows := congrArg (fun t => t * (rows : Int)) linear
  have poly_eq : 5 * (rows : Int) * (seats : Int) - 3 * (rows : Int) ^ 2 = 15 * (rows : Int) := by
    simpa [mul_comm (rows : Int) (seats : Int), mul_comm (rows : Int) (rows : Int)] using mul_rows
  rw [h0] at poly_eq
  -- 2250 - 3*rows^2 = 15*rows から整理して行列式を作る
  have poly : (rows : Int) ^ 2 + 5 * (rows : Int) - 750 = 0 := by
    -- from 5*450 - 3*r^2 = 15*r  => 3*r^2 + 15*r - 2250 = 0 => r^2 + 5*r - 750 = 0
    norm_num at poly_eq
    linarith

  -- 因数分解 (r-25)(r+30) = 0 を得る
  have factorization : ((rows : Int) - 25) * ((rows : Int) + 30)
                      = (rows : Int) ^ 2 + 5 * (rows : Int) - 750 := by ring
  have mul0 : ((rows : Int) - 25) * ((rows : Int) + 30) = 0 := by
    rwa [←factorization] at poly

  -- 整数での積が 0 ならどちらかの因子が 0。rows + 30 > 0 なので rows - 25 = 0 が成立する。
  have cases := Int.mul_eq_zero.mp mul0
  -- rows は自然数なので (rows : Int) + 30 > 0
  have pos : 0 < (rows : Int) + 30 := by
    exact add_pos_of_nonneg_of_pos (Int.coe_nat_nonneg rows) (by norm_num : (0 : Int) < 30)
  -- したがって二つ目の因子が 0 になることはない
  cases cases with
  | inl h => -- (rows : Int) - 25 = 0 の場合
    have : (rows : Int) = 25 := by linarith [h]
    -- 整数から自然数への同値化
    norm_cast at this
    exact this
  | inr h =>
    -- (rows : Int) + 30 = 0 は pos に矛盾
    linarith [pos, h]

というこであったが、なんか長いな。こちらもMathlibをimportしているので評価はできない。

ChatGPTにClaudeの回答を講評してもらった

そこで、ChatGPTにClaudeの回答をチェックしてもらった。

そして、次はzify

さらに、nlinarithが肝らしい。

総評として、Claudeの回答はLeanとしてはスマートにできているが、人間に対する可読性が低いと。

どうにかして、Mathlibを使えるようにしたいものだ。。

追記：Lean4webでチェックした

そういえば、Lean4webというのがあった。これはMathlabが組み込まれていて、評価ができる。

どうだろう、エラーは出ていない。

追記２：証明の過程をドキュメント化してもらった

Claude Codeにこの証明の過程をドキュメント化してもらった。

lean4-skillsの働きがよくわかる。成果物をここに供養する。