Article Source: New Wisdom
Recently, the math genius Terence Tao, who is enthusiastic about using GPT-4 and Copilot for research, has once again discovered a hidden bug in his paper with the help of AI!
Tao said that he found, while formalizing the argument on page 6 using Lean4, that the expression
is actually divergent when n=3, k=2.
This somewhat inconspicuous bug was caught in time, thanks to Lean4.
The reason is that Lean requires him to construct 02. As a result, Lean cannot be based on negative 0.
Fortunately, this is just a small bug that only exists when the value of n is very small. At this point, only a few constants in the paper need to be modified.
Some math enthusiasts and fans exclaimed in this post: "This is amazing! It's great to see the spread of AI proof assistants, laying a more solid foundation for the future of mathematical research."
Tao said that this is entirely possible.
Perhaps in the near future, we can build an AI layer on top of Lean.
Just describe each step of the proof to AI, and AI can use Lean to execute the proof, while also being able to call various computer algebra software packages during the process.
In June of this year, Tao had predicted in a blog post about his experience with GPT-4 trial:
By 2026, AI will combine with search and symbolic mathematical tools to become a reliable co-author in mathematical research.
Tao himself has also been practicing what he preaches, and has already started writing a new paper using GPT-4, repeatedly exclaiming about the amazing capabilities of GitHub Copilot, which makes him feel uneasy!
AI Empowers Mathematical Research by the Great Master
This month, Terence Tao has completely "dived into" AI.
With the help of GPT-4, he has started learning to write papers and conduct mathematical research using Lean4.
This process undoubtedly excites him, so he posts on Mastodon every few days (or even every few hours) to record his learning insights and experience.
In writing a paper on the study of the MacLaurin inequality, Tao made extensive use of AI tools such as GPT-4, Copilot, and Lean4.
Paper link: https://arxiv.org/abs/2310.05328
As of now, Tao has already completed the repair of the argument in the second section of the paper in Lean4.
However, this process is much more cumbersome than he had anticipated, taking about an hour to formalize each line of the proof.
In the first week of the project, his bottleneck was unfamiliarity with Lean syntax and tools; but the current bottleneck is the tools themselves—not as advanced as those in computer algebra software packages.
For example, in a line of the paper, he pointed out the inequality:
which can be rearranged as:
Assuming all denominators are positive, this is a very quick task for manual calculation, and can also be quite easily accomplished in any standard computer algebra software package.
Although Lean has very practical automatic tools for handling linear operations, it currently lacks automatic simplification tools for complex expressions involving exponents.
Therefore, we must handle exponent laws and the above operations step by step, which is very time-consuming.
Finally, Tao decided not to use asymptotic symbols in this part of the argument, but instead established an inequality with a determined constant C:
where
Initially, Tao thought it would be "simpler" to prove the inequality using values such as C=7. However, it was very cumbersome to rigorously prove C≤7 using existing tools, so he abandoned this idea and instead used a more operationally manageable C value. The selected numerical value is approximately 6.16.
In response, a curious netizen asked, "How does AI's proof speed compare to manual calculation?"
Tao said that, in his observation, tasks that are mechanical for computer algebra software packages and calculators are not necessarily mechanical for formal proof assistants.
But with the emergence of LLM, we should be able to unify all computer-aided tools into a very user-friendly general tool. And this tool will have all the advantages of each component.
Even in the near future, we can imagine building an AI layer on top of Lean—
By describing each step of the proof to AI in "mathematical English," AI can then attempt to use Lean to execute the proof, perhaps even calling computer algebra software packages during the process.
Copilot Can Even Guess the Next Steps
Previously, in the paper on the MacLaurin inequality study, Terence Tao was amazed to find that Copilot could predict what his next step would be!
It not only correctly predicted multiple lines of code used for routine verification, but also inferred the direction in which Terence Tao wanted to conduct research based on the theorem names he provided.
This made Terence Tao exclaim repeatedly: "It's incredible!"
In the process of proving Theorem 1.3 in the paper, Terence Tao formalized the proof using Lean4.
In the paper, the proof process only takes one page, but the formalized proof uses 200 lines of Lean4.
For example, in the paper, Terence Tao only assumed
is convex on any real number a>0, and later called the Jensen inequality. But the related code required almost 50 lines.
During this process, GitHub Copilot demonstrated various miraculous predictions, mysteriously inferring the direction of Terence Tao's research to come.
And Lean's rewriting strategy allows him to modify lengthy assumptions or goals through targeted replacements.
This feature is extremely important, as it allows people to manipulate these expressions freely without always having to input them in full.
In comparison, this operation is much more cumbersome in LaTex.
Terence Tao said that he needs to roughly simulate Lean4's rewriting strategy, by selectively editing lengthy expressions from one line to the next through operations such as cutting and pasting. This can lead to typos spreading across multiple lines in the document.
But Lean4 can accomplish this rewriting in an automatic and verified manner.
Of course, Lean 4 is not yet perfect and has some limitations. For example, rewriting expressions involving constrained variables is not always easy.
Terence Tao said he is looking forward to the day when he can easily request LLM to perform such transformations using natural language.
Diving into GPT-4 + GitHub Copilot, Crazy Recommendation
As early as early September, Terence Tao praised the effectiveness of ChatGPT in generating Python code—directly saving half an hour of work!
As an experiment, he asked ChatGPT to write a piece of Python code to calculate the length of the longest subsequence of 1,…,n for each natural number n, where the Euler totient function ϕ is non-decreasing.
For example, 𝑀(6)=5, because ϕ is non-decreasing on 1,2,3,4,5 (or 1,2,3,4,6), but not on 1,2,3,4,5,6.
Interestingly, it generated a very clever piece of code to calculate the totient function, which was so clever that Terence Tao had to stare at it for a few minutes to understand the underlying principle behind the code.
Of course, this code has its biases—it only considers subsequences of consecutive integers, not arbitrary subsequences.
However, this was close enough, and using the initial code generated by ChatGPT as a starting point, Terence Tao eventually manually generated the code he wanted, saving him approximately half an hour of work.
Because the results from ChatGPT were very good, Terence Tao said he would frequently use it in the future to provide initial code for similar calculations.
Soon after, Terence Tao posted again, saying that he had been recommended to try out GitHub Copilot by a friend!
As expected, Copilot's subsequent performance truly delighted him—just giving a brief introduction and a sentence, AI recommended content that was very close to his own ideas.
With only slight modifications to these suggestions, he was able to complete the work in less than half the time originally planned.
In October, while researching natural number games, Terence Tao found that although GPT-4 could not directly help with the game, it became very useful when he started using Lean.
As the levels became increasingly difficult, the role of GPT began to gradually manifest.
In cases where it was obvious that Z was the result of X and Y, asking GPT "How can I prove Z if I already know X and Y" could solve various subtle syntax issues in the process.
In addition to professional content, after discovering that he could use DALL·E 3, Terence Tao immediately started playing with it.
Netizens: LLM Can Make Outstanding People 10,000 Times Better
The great master's obsession with AI tools in mathematical research has also sparked heated discussions among netizens.
Someone said that the great master started learning Lean4 with the help of GPT-4 at the beginning of this month, and occasionally recorded his learning progress on Mastodon.
This also indicates that for the most successful people, LLM can accelerate their work.
Someone said that even people who cannot write code, as long as they are excellent LLM communicators, can quickly achieve automation of functionality.
However, if only highly skilled people can effectively use LLM, the result may exacerbate inequality between people.
Immediately, someone came forward to say that this is true. A friend of theirs could not write anything other than Excel formulas before, but now they can write Python applications using GPT-4!
And as a coder with 30 years of development experience, they even had to ask their friend to teach them this technology.
His success is probably because he is very good at communicating with LLM.
Someone predicted that over time, people using LLM will gain overwhelming benefits, regardless of their intelligence, and they will climb higher and higher on the ladder, becoming experts in their field.
For elites, they may receive 100 times the assistance from LLM, and for top engineers, this assistance may be about 10,000 times.
Reference: https://mathstodon.xyz/@fanf42@treehouse.systems/111294362321849062
免责声明：本文章仅代表作者个人观点，不代表本平台的立场和观点。本文章仅供信息分享，不构成对任何人的任何投资建议。用户与作者之间的任何争议，与本平台无关。如网页中刊载的文章或图片涉及侵权，请提供相关的权利证明和身份证明发送邮件到support@aicoin.com，本平台相关工作人员将会进行核查。
