速報
ProofWala：跨平台多語言證明工程框架加速 Lean 與 Rocq 互動
研究背景指出現有證明工具多為助理專屬且僅支援檔案層級執行。ProofWala 以 itp-interface 為基礎，提供跨 Lean 4 與 Rocq 的程式化互動層，支援全倉庫的 tactic 追蹤與依賴抽取。實驗顯示跨語言訓練提升 Lean Mathlib 與 CategoryTheory 的證明搜尋效能。
速報
研究背景指出現有證明工具多為助理專屬且僅支援檔案層級執行。ProofWala 以 itp-interface 為基礎，提供跨 Lean 4 與 Rocq 的程式化互動層，支援全倉庫的 tactic 追蹤與依賴抽取。實驗顯示跨語言訓練提升 Lean Mathlib 與 CategoryTheory 的證明搜尋效能。
深度分析
本文以一個可檢視的案例，報告使用 Aristotle API 結合 Lean 4 嘗試形式化 IMO 2009 的 Grasshopper 組合問題。Aristotle 產出一套 Lean 檔案，成功驗證四個局部輔助引理（包含最終和式、相鄰交換的影響與最大化引理），但主定理以未證明的 placeholder（sorry）收尾。