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 Workbook: A large-scale Lean problem set formalized from natural language math problems
Shanghai AI Laboratory（上海人工智能实验室）；Tsinghua University（清华大学）；Shanghai Jiao Tong University（上海交通大学）；Peking University（北京大学）；The Chinese University of Hong Kong（香港中文大学）
Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs
D-CHAB, ETH Zurich, Zurich, Switzerland.；D-INFK, ETH Zurich, Zurich, Switzerland.；ETH AI Center, Zurich, Switzerland.；University of Pennsylvania, PA, USA.；Independent Researcher.
Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4
State Key Laboratory for Multimedia Information Processing, School of Computer Science, PKU-Anker LLM Lab, Peking University（信息处理国家重点实验室，计算机科学学院，PKU-Anker LLM实验室，北京大学）；Huawei Technologies Co., Ltd.（华为技术有限公司）；School of Software & Microelectronics, Peking University（软件与微电子学院，北京大学）；School of Electronics Engineering and Computer Science, Peking University（电子工程与计算机科学学院，北京大学）
Combining Textual and Structural Information for Premise Selection in Lean
Faculty of Mathematics and Physics, University of Ljubljana（卢布尔雅纳大学数学与物理学院）；University of Ljubljana（卢布尔雅纳大学）；Department of Knowledge Technologies, Jožef Stefan Institute（知识技术系，乔泽夫·斯塔芬研究所）
LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization
Department of Statistics, University of Warwick, UK（英国沃里克大学统计系）；Center for Advanced Intelligence Project, RIKEN, Japan（日本理化学研究所高级智能项目）；Department of Statistics, University of Michigan, USA（美国密歇根大学统计系）；Department of Mathematical Informatics, The University of Tokyo（东京大学数学信息学系；日本理化学研究所高级智能项目）；also Center for Advanced Intelligence Project, RIKEN, Japan（加州大学伯克利分校电气工程与计算机科学系；统计系）；Department of Electrical Engineering and Computer Sciences, also Department of Statistics, University of California, Berkeley, USA（上海交通大学数学科学学院，自然科学院和MOE-LSC）；School of Mathematical Sciences, Institute of Natural Sciences and MOE-LSC, Shanghai Jiao Tong University, China
