Shulou(Shulou.com)12/24 Report--

[introduction to Xin Zhiyuan] after three weeks, Tao Zhe-Xuan successfully completed the process of proving the formal polynomial Freiman-Ruzsa conjecture with the AI tool. He once again called on mathematics researchers to learn to use AI tools correctly, and netizens exclaimed: there is no need for human beings to read math papers in the future.

Using AI tools to assist in the research of mathematics projects was once again run by Tao Zhe Xuan!

Three weeks ago, he posted a blog post documenting the process of proving the formal Freiman-Ruzsa conjecture in Lean4 using Blueprint.

Just yesterday, he excitedly announced that the Lean4 project, which formalized the proof of polynomial Freiman-Ruzsa conjecture, was a success three weeks later.

Now that the dependency graph is completely covered in green, the Lean compiler reports that this conjecture fully follows the standard axiom.

Tao Zhe Xuan said that in the whole team, he contributed only about 5% of the code. This result is encouraging because it means that mathematicians can lead formal projects for Lean even if they do not have Lean programming skills.

He found that the most mathematically interesting parts of the project were easier to formalize, while the most technically obvious steps were the most time-consuming.

Using Blueprint to break down the project into small to moderate parts works well, which makes it possible to do a lot of parallel work.

In this way, many contributors can deal with specific subtasks without having to understand the whole proof process or even have no knowledge of the relevant mathematical domain.

Just a few minutes ago, Lean successfully proved the PFR conjecture without leaving any outstanding questions ("sorry" will be mentioned later). This means that all the main objectives of the project have been successfully completed.

At the same time, his blog post on November 18, three weeks ago, was also published by netizens, causing a heated discussion.

Sure enough, it will take months for people to realize that AI reinforces the subversive power of mathematical research.

And only the researchers at the forefront can feel the impact and shock of this great force at the first time.

Tao Zhe Xuan appealed: mathematicians must learn to use AI. Some netizens asked Tao Zhe Xuan: does this mean that there are more and more proofs that human beings cannot understand, but machines can solve them?

On the contrary, if the formalization of proof becomes more mainstream and more AI-assisted, it is entirely possible to create proof that is both human-readable and machine-readable, Tao says.

The blueprint proved by PFR proves this point-- both human readable, each proof step has a formal reason, and a dependency graph can be obtained to visualize the global structure of the whole argument.

Of course, Tao Zhe Xuan also cautioned not to confuse "computer-aided proof" with "unable to provide understanding / accidental proof".

For example, more than 10000 pages of proof of finite simple group classification is almost 100% artificially generated, but an alternative proof processed by a computer is more satisfactory in some ways.

After several rounds of discussion with netizens, Tao Zhe Xuan made the following summary--

Blueprint itself is a programming language and can be regarded as a kind of pseudocode of Lean.

Many mathematicians should change their writing style from standard mathematical English / LaTex to Blueprint / LaTex.

Netizens: future research does not need to be "human readable". AI can understand it. Netizens said that Tao Zhe Xuan's random mastery of various research tools can almost be called terrible.

When I tried math in graduate school, it was like a caveman shaking an ordinary unicycle when suddenly a helicopter appeared in front of my eyes, and the man held out his hand to me and told me to give it a try.

Ever since I heard about the four-color theorem, I have always known that formalization is the future of mathematics. But what I didn't expect was that Tao Zhe Xuan was so leisurely and formalized that he could do almost all his math writing with AI as soon as he gained traction.

Formalization refers to the real derivation of each statement in the proof from the basic axioms and rules. In this blog post, Tao Zhe Xuan abstracts all the work that needs to be memorized and gives it to the machine.

His work shows that formalization is only just beginning to attract attention in mainstream mathematics.

Some people have begun to imagine that there will probably be a time when most of the proof is done in Lean or similar systems, and no one will ever bother to write a "human readable" paper.

Mathematics will become a kind of programming!

A master of mathematics said that his own research steps now have three steps--

1. Understand what you are trying to prove, by reading or talking to people

two。 Draw a sketch with paper and pen that contains the main points

3. Input the proofs into LaTeX to make the homework you have to hand in human readable.

Yes, if we just want to train or fine-tune AI to produce answers, and then write a loop to feedback until the compiler outputs correctly, then we don't really need to understand.

In this way, we can generate more training examples, and we can manually check whether the results meet the requirements and make comments. Training can improve the accuracy of the initial answer.

The formalization process of PFR conjecture the following is the formalization process of Tao Zhe Xuan posted on his blog, which can be challenged by interested readers.

In November, Tao Zhe Xuan launched a collaborative project with Yael Dillies and Bhavik Mehta to formalize his previous preprinted paper on Freiman-Ruzsa (PFR) conjecture using Lean4.

Although the project has been launched for less than a week, it is going quite well and most of the files have been formalized.

The project benefits from Patrick Massot's Blueprint tool, which enables the team to write a human-readable proof "blueprint" that is closely related to Lean formalization.

One of Tao Zhe Xuan's favorite features in Blueprint is the automatically generated dependency graph. It provides a rough snapshot of the progress of formalization. As of that time, the dependency graph looks like this:

In the legend that depends on the graph, different bubbles (representing lemmas) and rectangles (representing definitions) are given different colors.

Simply put, green bubbles or rectangles represent lemmas or definitions that have been fully formalized, while blue ones refer to lemmas or definitions that are ready to be formalized (which means that their statements have been formalized but have not been proved yet. the same is true of all relevant prelemmas and proofs).

The goal of Tao Zhe Xuan's team is to turn all the bottom bubbles that lead to "pfr" bubbles green.

When you click the "pfr" bubble at the bottom of the dependency figure, you can see the following:

In the figure, Blueprint shows a form of human-readable PFR statement, along with a human-readable proof of the statement, which depends on other statements in the project:

Note that the "pfr" bubble is white, but has a green border, which means that PFR's statement has been formalized in Lean, but it has not been proved.

The proof itself is not ready to be formalized because some prerequisites (especially "entropy-pfr" Theorem 6.16) are not even formally stated.

Click the Lean link under the PFR statement in the dependency diagram to enter the appropriate Lean document:

This is what the typical theorem in Lean looks like. There are many assumptions before the colon, such as:

G is a finite elementary Abelian group belonging to order 2 (this is how the team chooses to formalize the finite field vector space), An is a non-empty subset of G, and the cardinality of Abelian An is less than K times the cardinality of A.

The statement after the colon is the conclusion: a can be included in the subgroup H of G in the form of the sum of 2K12 H, as well as in the set c of the cardinality of the largest number.

Smart readers may notice that the above theorem seems to lack one or two details, for example, it does not explicitly assert that H is a subgroup.

This is because the "pretty printing" pattern suppresses some of the information in the theorem statement, which can be seen by clicking the "Source" link.

As you can see, H needs to have the type of G addition subgroup.

There is an obvious "sorry" at the bottom of the theorem, which means that the theorem has not been proved yet, but the ultimate intention is, of course, to replace the "sorry" with an actual proof.

Filling this "sorry" is still hard to do, so you need to find a simpler task.

Here is a simple intermediate Lemma "ruzsa-nonneg", which appears in the proof:

The expression d [Xternal Y] refers to the entropy Ruzsa distance between X and Y, which is a real number.

The bubble is blue with a green border, which means that the statement has been formalized and the proof is ready to be formalized.

The Blueprint dependency diagram shows that this Lemma can be derived from the previous Lemma, called "ruzsa-diff":

"uzsa-diff" is also blue and the border is green, so it has the same current state as "ruzsa-nonneg": the statement is formal and the proof is ready to be formalized, but the proof has not yet been written in Lean. Where H [X] is the Shannon entropy of X.

By looking at Lemma 3.11 and Lemma 3.13, we can clearly see that | H [X]-H [Y] | is obviously non-negative.

So even if we don't know how to prove Lemma 3.11, it should be easy to assume that Lemma 3.11 holds and complements the proof of Lemma 3.13.

The formalization of Lemma 3.11 is as follows: ("sorry" means that Lemma has not yet proved it)

At the same time, Lemma 3.13 is formalized as:

Now, we're going to try to fill in the latter "sorry".

In the local copy of the PFR github repository, Tao Zhe Xuan opens the relevant Lean file with an editor (Visual Studio Code, with the extension lean4) and navigates to the "sorry" of "rdist_nonneg".

The accompanying Lean Information View shows the current status of the Lean certificate:

At the bottom, you can see the goal we need to prove.

Next, in proving this claim, a series of "tactics" need to be used to change goals and / or assumptions.

The first step is to add the factor 2 required to apply Lemma 3.11.

Now, we have two goals (and two "sorry"): one is to prove that 0 ≤ 2d [X * * Y] is equivalent to 0 ≤ d [X * * Y], and the other is to prove 0 ≤ 2d [X * * Y].

The status after filling in the first "sorry" is as follows (some extraneous assumptions deleted):

A very convenient "linarith" strategy can be used here, which can solve any goal that can be obtained from the linear operation of existing assumptions:

After success, you can see that the status report shows that the branch no longer has a goal to prove. So, let's continue with the rest of the "sorry", that is, to prove 0 ≤ 2d [XTX Y]:

Here, we will try to reference Lemma 3.11. To do this, Tao Zhe Xuan added a few lines of code:

So, we have two more sub-goals, one is to prove the constraint.

(it can be called "h"), and the other is to derive the former goal 0 ≤ 2d [XTX Y] from h.

For the first target, you need to call the "diff_ent_le_rdist" Lemma that is coding Lemma 3.11.

One way to do this is to try to use the "exact?" strategy, which automatically searches to see if the target can be immediately deduced from the existing Lemma:

So Tao Zhe Xuan clicked on the suggested code (the system will automatically paste it into the correct location). As a result, it succeeded, leaving only the last "sorry":

Here, Tao Zhe Xuan General uses the "exact?" strategy and establishes a matching boundary as recommended.

:

In completing the last "sorry", Tao Zhe Xuan tried "exact?" again to know how to combine h and h' in order to achieve the desired goal, and it was a success!

As you can see, all the underlines are gone. In other words, Lean has regarded it as valid proof.

By omitting a few intermediate steps, we can compress this proof quite compactly:

Now it's proved to be done!

What we end up with is basically a "one-line proof", which is reasonable considering that Lemma 3.11 and Lemma 3.13 are so close.

Then, Tao Zhe Xuan pushes all the content back to the Github main version library.

Rebuilding Blueprint takes quite a long time (about half an hour), and the dependency graph now shows "ruzsa-nonneg" in green:

So it can be said that the formalization of PFR is closer to completion.

However, although "ruzsa-nonneg" is now painted green, there is no complete evidence of this result, because the Lemma "ruzsa-diff" it relies on is not green.

From this point of view, the proof is still partially completed.

Tao Zhe Xuan expressed the hope that at some point in the future, the previous results can also be proved, at that time, it can be said that the result of PFR's conjecture has been completely proved.

Reference:

Https://news.ycombinator.com/item?id=38528582

Https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/

This article comes from the official account of Wechat: Xin Zhiyuan (ID:AI_era)

Welcome to subscribe "Shulou Technology Information " to get latest news, interesting things and hot topics in the IT industry, and controls the hottest and latest Internet news, technology news and IT industry trends.