要約
リーン 4 のようなコンピューター化された検証可能な形式言語を使用して数学的定理を証明することは、数学的な形式化に大きな影響を与えます。
Lean 4 は、数学的推論を進歩させるための顕著な可能性を提供します。
ただし、既存の取り組みは、実質的なオンライン コーパスにおける数学的形式化言語に限定されており、急速に進化する言語に遅れをとらないようにすることに専念しています。
従来の証明とコンピュータ化された証明の間のギャップを埋めるために、定理証明の形式化に対する私のアプローチには、自然言語 (NL) 証明に基づく大規模言語モデル (LLM) を使用して形式的なステップを生成し、証明を完了することが含まれます。
この方法では、一般的な基本構造と戦術を紹介し、AI が数学的形式化プロセスを支援してそのパフォーマンスを向上させる方法を決定し、主に IMO での NL と比較したリーン 4 の問題解決の例と、サンプル定理の証明を示します。
抽象代数。
要約(オリジナル)
Using computerized verifiable formal languages like Lean 4 to prove mathematical theorems has a significant impact on mathematical formalization. Lean 4 offers prominent potential for advancing mathematical reasoning. However, existing efforts are limited to mathematical formalization languages in substantial online corpora and are dedicated to keeping pace with rapidly evolving languages. To bridge the gap between the traditional and computerized proof, my approach to formalizing theorem proving involves generating formal steps and complete proofs using Large Language Models (LLMs) based on Natural Language (NL) proofs. The method is to introduce the basic structure and tactics in general, determine how AI can assist the mathematical formalization process to improve its performance, and give examples of solving problems in Lean 4 comparing to NL, mainly in IMO, and a sample theorem proving in abstract algebra.
arxiv情報
| 著者 | Xichen Tang |
| 発行日 | 2024-10-31 16:01:59+00:00 |
| arxivサイト | arxiv_id(pdf) |
提供元, 利用サービス
arxiv.jp, Google