要旨：入念に校正された論文であっても、証明や明示された仮定にわずかな隙間が残ることがあります。私たちはPaperFormalizerを提案します。これはLeanベースのエージェント型パイプラインで、著者が自らの論文におけるこうした隙間を見つけ出し、埋めることを支援し、各論文をLeanで検証済みのバージョンへと変換します。LaTeXソースから出発し、PaperFormalizerは論文を命題の依存関係グラフに変換し、各命題について自然言語による忠実性・曖昧さ・正確性の審査を行い、さらにMathlibや任意の領域ライブラリ、著者の個人用ツールキットに対し、Leanで形式化・証明を行います。ある命題が何を意図しているのか、また結果における形式化上のギャップをどのように修正するのが最善かを知るのは、あくまで著者だけです。そのため、一つの命題が複数の解釈を許す場合、パイプラインは一時停止して著者に確認を求めます。そして、自然言語とTeX記号を用いて各修正案を提示し、著者はこれを承認・却下・再指示のいずれかを選択できます。さらに、論文が主張する内容を潜在的に変える可能性のあるあらゆる判断は、すべて著者に委ねられます。最終的な成果物は、注釈付き・改訂版の論文、変更点の報告書、および各宣言がその形式化対象の命題とリンクされるLeanコードです。多くの論文が形式化されるにつれて著者のツールキットは拡充され、著者は自身の検証済み論文を共有することで、それを基に研究を進める研究者がそのLeanコードを再利用できるようになります。検証済み論文の作成を実用的にすることにより、PaperFormalizerは数学的証明に依拠する研究の信頼性向上を目指しています。PaperFormalizerはコーディングエージェント（Claude CodeまたはCodex）内にて動作し、こちらのhttps URLでご利用いただけます。ユーザーによって共有されたLeanコードを含む論文は、こちらのhttps URLでご覧いただけます。
投稿履歴
論文へのアクセス：
PDFを表示
HTML（実験的）
TeXソース
追加機能
音声要約
現在の閲覧コンテキスト：
参考文献・引用
Google Scholar
Semantic Scholar
ブックマーク
機関
arXivLabsは、共同作業者が当社のウェブサイト上で新しいarXiv機能を直接開発・共有できるフレームワークです。
arXivLabsを利用する個人および組織は、オープン性、コミュニティ、卓越性、そしてユーザーデータのプライバシーという当社の価値観を積極的に受け入れ、尊重しています。arXivはこれらの価値観に固くコミットしており、それらを遵守するパートナーのみと協力しています。
arXivのコミュニティに価値をもたらすプロジェクトのアイデアをお持ちですか？arXivLabsについて詳しくご覧ください。