Lean-Mathematical formal proof tools and AI automated proofs

With the development of computer technology, various disciplines are committed to promoting the combination of disciplines and computer AI technology, mathematics is no exception, as one of the most important basic disciplines in the world, mathematicians are also actively trying the integration of mathematics and AI technology, one of the very popular directions is to promote the automatic proof of mathematics, with the help of AI to promote the further development of mathematics discipline, and inject new blood into mathematics discipline. But there exist some difficulties in the mathematical proving because of the differences between the Mathematical Logic and Computer Logic. To overcome the difficulties, Mathematician and computer scientist created many tools, like lean and Lean Copilot. Lean has a powerful type system and efficient proof capabilities. Lean Copilot, on the other hand, offers intelligent code suggestions and supports a variety of tasks, among many other advantages. In this paper, we will introduce the tool of mathematical formalization, LEAN, as well as the development process and future direction of mathematical automated proofs.