Terence Tao uses large-scale model proof assistant Lean to show his preference

"I predict that, if used correctly, AI will become a trusted co-author in mathematical research and many other fields by 2026." Mathematician Terence Tao said in a previous blog.

Tao Zhexuan said this and did it.

He has recently been conducting mathematical research using tools such as GPT-4, Copilot, and Lean, and also discovered a hidden bug in his paper with the help of AI.

Recently, Terence Tao stated that the Lean4 project has successfully completed the formalization of the proof of the Polynomial Freiman-Ruzsa Conjecture (PFR), which took only three days. week. At the same time, the Lean compiler also reports that the conjecture conforms to the standard axioms. This is a great success proved by computers and AI, and it is exciting

For more information about the above research, interested readers can Refer to "What is Tao Zhexuan's formal proof using AI?" Understand the past and present life of PFR conjecture in one article.

Seeing this, careful readers may have discovered the clue. Master Tao mentioned Lean many times when conducting mathematical research. Simply put, Lean is a programming language that helps mathematicians verify theorems, where users can write and verify proofs. Compared with the original Lean, the latest Lean 4 version has many optimizations, including a faster compiler, improved error handling, and better integration with external tools.

Lean is widely used in the field of mathematics. Today, when large models (LLM) are popular, is there a better way to combine the two?

Now someone has realized it, the open platform LeanDojo team (for LeanDojo, please refer to "AI large model helps Tao Zhexuan solve problems, and can also prove mathematics Theorem? ") and researchers from the California Institute of Technology launched Lean Copilot, a collaboration tool designed for LLM and human interaction, aiming to provide 100% accurate formal mathematical proof.

It is worth noting that the LeanDojo team’s research mainly focuses on using LLM to automate theorem proving. From this point, it is not difficult to see that they launched It's not surprising that Lean Copilot is related to LLM.

Project address: https://github.com/lean-dojo/LeanCopilot

For This research, apart from saying it is cool, is very cool, and the evaluation is still very high.

Use LLM in Lean to speed up mathematical proof

For a long time, automated theorem proving has been faced with Due to many difficulties, mathematical proofs traditionally rely on manual derivation and require careful verification. Now with the advancement of AI, researchers have begun to use artificial intelligence to conduct in-depth exploration, but this problem is inevitable, that is, LLM is sometimes not very reliable in mathematics and reasoning tasks, and is prone to errors and hallucinations.

The function of Lean Copilot allows users to use large language models to automate the proof process in Lean and improve the speed of proof synthesis. When needed, users can also seamlessly intervene and modify to achieve balanced collaboration between machine intelligence and human intelligence

Using Lean Copilot, LLM can be used in Lean to achieve proof automation , including strategy suggestions, premises and search proofs

Users can choose to use the built-in models provided by LeanDojo, or import their own models. These models can be run locally (with or without a GPU), or in the cloud

#In short, Lean Copilot provides users with a flexible way to enhance it by introducing LLM and optimize the process of theorem proving in Lean.

The main features of Lean Copilot can be summarized as:

• LLM is able to propose proof steps, search for proofs, and select useful lemmas from a large mathematical library.
• Lean Copilot can be set up as a Lean package and runs seamlessly within a Lean VS Code workflow.
• Users can use the built-in models in LeanDojo, or use their own models, which can be run locally (with or without GPU) or in the cloud.
• The tool runs on a variety of platforms, including Linux, macOS, and Windows WSL.

To make LLM more accessible to Lean users, Lean Copilot hopes to start a positive feedback loop: proving that automation will lead to better data and ultimately improve LLM’s performance in mathematics performance.

Copilot’s effect demonstration

You can configure Lean Copilot according to the official tutorial. After the configuration is completed, you can start the experiment. The author of the project also provides some official examples for reference

Recommended solutions. After importing LeanCopilot, you can use suggest_tactics to generate recommended solutions. During use, you can also click on the recommended solution and use it in the proof (refer to the image below)

You can use a prefix, For example, simp, to limit the generated strategy

search proof. Use search_proof to combine LLM-generated policies with aesop (Lean 4’s white-box automation project) to search for multiple policy proofs. Once you find the proof, you can click on the strategy to insert it into the editor

Rewritten content: Choosing the premise is an important one Strategy. The purpose of this strategy is to retrieve a list of potentially useful premises. Currently, Lean Copilot will use the search tool in LeanDojo to select premises from the fixed snapshot of Lean and mathlib4 (i.e., Lean 4 math library)

You can run LLM. Whether it's theorem proving or other reasoning, you can run LLM in Lean. You can run any model locally or remotely (see Bring Your Own Model)

Some advanced usages are also mentioned in the project for interested readers , you can go to the original project to learn more.

The above is the detailed content of Terence Tao uses large-scale model proof assistant Lean to show his preference. For more information, please follow other related articles on the PHP Chinese website!