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.

翻译：使用Lean 4这类可计算机验证的形式化语言来证明数学定理，对数学形式化领域具有重要影响。Lean 4在推进数学推理方面展现出显著潜力。然而，现有工作主要局限于大规模在线语料库中的数学形式化语言，且致力于跟上快速演进的语言发展。为弥合传统证明与计算机化证明之间的鸿沟，本文提出的定理证明形式化方法，旨在基于自然语言证明，利用大语言模型生成形式化步骤与完整证明。该方法通过总体介绍基本结构与策略，确定人工智能如何辅助数学形式化过程以提升其性能，并以国际数学奥林匹克竞赛问题为主，给出Lean 4与自然语言对比求解的实例，并展示抽象代数中的定理证明示例。