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.

翻译：使用Lean 4等计算机验证语言对数学证明进行形式化，具有显著影响数学领域的潜力，它为推进数学推理提供了卓越的能力。然而，现有的工作主要局限于从海量在线数学语料库中创建证明的形式化版本，难以跟上数学快速发展的步伐。为了弥合传统证明技术与计算机化证明技术之间的差距，本文探索了使用大型语言模型生成形式化证明步骤及完成形式化证明的方法。通过将自然语言数学证明转换为形式化版本，本工作介绍了Lean 4语言的基本结构和策略。其目标是确定如何利用人工智能来辅助数学形式化过程并提升其性能。本文提供了多个示例，分别展示了使用传统方法和基于Lean 4的方法来解决问题。最终，本文阐述了对Lean 4基础的说明，并对使用传统技术与AI增强技术进行数学形式化的过程进行了比较分析。研究结果表明，AI驱动的工具在加速和增强数学证明形式化方面具有巨大潜力，为未来AI for Math实现更高效、更可靠的定理证明铺平了道路。