Yanasse：Deep Visionのアナロジーから新しい証明を見つける（第1部）

要旨: Project Yanasse は、数学の構造的に離れた領域から、証明戦略パターン（例: Lean 4 の tactic 呼び出しパターン）を移すことで、ある数学領域における定理の新しい証明を発見する方法を提示する。システムは、Mathlib の 27 の主要分野（217,133 の証明状態）にわたる tactic の使用分布を抽出し、ソース領域では大いに使われるがターゲット領域では希少または存在しない tactic を特定するために z-score を計算し、GPU 加速された NP 困難な類推（Apple の MPS バックエンドを介して MacBook Air 上で実行）によってソースとターゲットの証明状態を対応付ける。そして、その後 AI 推論エージェントに対し、ソースの tactic 呼び出しパターンをターゲットの定理へ「記号を置換するのではなく」意味的に適応させるよう求める。本研究の第一部では、この手法を Probability → 表現論 の組に適用し、10 回の試行から 4 つの Lean で検証された新しい証明（40%）を得た。これらの証明はいずれも sorry 宣言なしでコンパイルできる。主要な発見は、tactic スキーマは head（領域ゲート付きで、移送はめったに起きない）と modifier（領域汎用で、移送されやすい）に分解できるという点である。filter upwards の head は表現論では失敗する（Filter 構造がない）が、{LIST} と {w} modifier を伴う [LIST] は ext1 + simp [LIST] + rfl としてきれいに移送される。決定的なのは、基盤となるマッチングエンジン—deep vision lib.py—が完全に領域非依存であることだ。同じ最適化コードが、類推によってチェスの局面を対応付ける NP 困難なマッチングに対しても、類推によって Lean の証明状態を対応付ける場合にも用いられ、処理対象の領域が何であるかを知らなくても動作する。領域に特化しているのは関係抽出器だけである。