PaperFormalizer：リーンにおける研究論文の著者参加型自動形式化

arXiv:2610.31810v1 発表タイプ：新規 要旨：入念に校正された論文であっても、証明や明示された仮定に小さな抜け穴が残ることがあります。私たちはPaperFormalizerを提案します。これはLeanベースのエージェント型パイプラインで、著者が自らの論文におけるこうした隙間を見つけ出し、埋めるのを支援し、各論文をLeanによって検証済みのバージョンへと変換します。LaTeXソースから出発し、PaperFormalizerは論文を命題の依存関係グラフに変換し、各命題について自然言語による忠実性・曖昧さ・正確性を審査した後、Mathlibや任意のドメインライブラリ、さらに著者の個人的なツールキットを参照して、命題を形式化し、Lean上で証明を行います。ある命題が何を意図しているのか、また結果における形式化上のギャップをどのように解消するのが最善かを知るのは、あくまで著者だけです。そのため、このパイプラインはそこで一時停止し、著者に問いかけます…