Leanの型理論をDeduktiで表現し、証明の移植を支援する

この論文をやさしく読む

ひとことで言うと

Leanで記述した数学の証明を他の証明支援系でも利用しやすくするため、その項と型をDeduktiで表す方法を示した研究です。

何に役立つ？

Leanの数学ライブラリを他のシステムに移す際の基盤になります。型を付けられるという性質を変換後も保つことが、形式的な記述を移植するうえで役立ちます。

この研究の面白いところ

単に記法を置き換えるだけでなく、変換先の理論を定め、型付け可能性を保存する変換として扱っています。

どこまで分かった？

対象はLean全体ではなく、そのかなり大きな部分集合です。要旨には対応する機能の具体的な範囲や、ライブラリ全体の移植実績は記載されていません。

v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。

アブストラクトの日本語訳

証明支援系Leanには、他の証明支援系の利用者にとっても関心のある、豊富な数学の形式化ライブラリがある。このライブラリを他のシステムへ変換する作業を支援するため、本研究では、Leanの項と型を符号化できる理論を論理フレームワークDedukti内に提示する。また、Leanのかなり大きな部分集合からこのDedukti理論への、型付け可能性を保存する変換を定義する。

v1の要旨から自動生成。本文の精読・人による確認は未実施。