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

TL;DR

This paper explores leveraging Large Language Models to convert natural language mathematical proofs into formal Lean 4 proofs, aiming to accelerate and improve the process of formalizing mathematics with AI assistance.

Contribution

It introduces a method for using AI to translate natural language proofs into Lean 4 formalizations, bridging the gap between traditional and computerized proof techniques.

Findings

AI tools can significantly speed up proof formalization.

AI-augmented formalization improves reliability and efficiency.

Demonstrated successful conversion of natural language proofs into Lean 4.

Abstract

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.