Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4

要約

Lean 4 のようなコンピューター化された検証言語を使用して数学的証明を形式化すると、数学の分野に大きな影響を与える可能性があり、数学的推論を進歩させるための優れた機能が提供されます。
しかし、既存の取り組みは主に、広範なオンライン数学コーパスから形式化されたバージョンの証明を作成することに限定されており、急速に進化する数学の性質に追いつくのに苦労しています。
従来の証明技術とコンピュータ化された証明技術の間のギャップを埋めるために、この論文では、正式な証明ステップを生成し、正式な証明を完了するための大規模言語モデル (LLM) の使用について検討します。
この作品では、自然言語 (NL) の数学的証明を形式化されたバージョンに変換することで、リーン 4 言語の基本構造と戦術を紹介します。
目標は、数学的形式化プロセスを支援し、そのパフォーマンスを向上させるために AI をどのように活用できるかを決定することです。
従来のアプローチとリーン 4 ベースのアプローチの両方を使用して問題を解決する例をいくつか示します。
最後に、このペーパーでは、リーン 4 の基礎の説明と、従来の手法と AI で強化された手法を使用した数学的形式化プロセスの比較分析を示します。
この調査結果は、AI を活用したツールには数学的証明の形式化を加速および強化する大きな可能性があり、将来的には AI for Math のより効率的で信頼性の高い定理証明への道が開かれることを示しています。

要約(オリジナル)

Formalizing mathematical proofs using computerized verification languages like Lean 4 has the potential to significantly impact the field of mathematics, it offers prominent capabilities for advancing mathematical reasoning. However, existing efforts are largely limited to creating formalized versions of proofs from extensive online mathematical corpora, struggling to keep pace with the rapidly evolving nature of mathematics. To bridge the gap between traditional and computerized proof techniques, this paper explores the use of Large Language Models (LLMs) to generate formal proof steps and complete formalized proofs. By converting natural language (NL) mathematical proofs into formalized versions, this work introduces the basic structure and tactics of the Lean 4 language. The goal is to determine how AI can be leveraged to assist the mathematical formalization process and improve its performance. Several examples are provided that demonstrate solving problems using both traditional and Lean 4-based approaches. Ultimately, this paper presents an explanation of the foundations of Lean 4 and comparative analyses of the mathematical formalization process using traditional and AI-augmented techniques. The findings indicate that AI- powered tools have significant potential to accelerate and enhance the formalization of mathematical proofs, paving the way for more efficient and reliable theorem-proving for AI for Math in the future.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google