How Did the World's Top Mathematicians Spend the May Day Holiday?
Fields Medal winner Terence Tao seems to be busy releasing his open-source project: "With the assistance of a large model, I wrote a proof-of-concept software tool to verify whether a given estimate involving arbitrary positive parameters holds (within a constant factor)."
Project address: https://github.com/teorth/estimates
In this project, Tao developed a framework for automatically (or semi-automatically) proving estimates in analysis. Estimates are inequalities in the form of X≲Y (representing X=O(Y) in asymptotic notation) or X≪Y (representing X=o(Y) in asymptotic notation).
Why create such a tool? This stems from a recent discussion between Tao and Bjoern Bringmann (Tao's former doctoral student, now an assistant professor at Princeton University).
For many mathematical tasks in algebra, calculus, and numerical analysis, symbolic mathematics packages are already quite "developed". However, there is currently no similar complex tool to verify asymptotic estimates - inequalities that should hold for arbitrarily large parameters without loss. Especially important are function estimates where parameters involve an unknown function or sequence (existing in a suitable function space).
Tao wrote about their discussion in a blog post, focusing on simpler asymptotic estimate cases involving a finite number of positive real numbers, combined using arithmetic operations like addition, multiplication, division, exponentiation, minimum, and maximum (but excluding subtraction).
"I had previously hoped for a tool that could automatically determine whether such estimates hold (providing a proof if true, or an asymptotic counterexample if false)."
Now, this wish has been realized.
We all know that Tao loves using large models to assist in solving mathematical problems. In the past, most cases involved completing relatively simple coding tasks, such as calculating and plotting somewhat complex mathematical functions or performing basic data analysis on certain datasets.
This time, he decided to give himself a more challenging task: writing a verifier that can handle the aforementioned inequality forms.
For example, a typical inequality might be the weak arithmetic mean-geometric mean inequality.
Where abc are arbitrary positive real numbers, and
Indicates our willingness to lose an unspecified (multiplicative) constant in the estimate.
In principle, such simple inequalities can be automatically solved through powerful case splitting. While individually these are not difficult to solve manually, some applications require verifying many such inequalities or splitting them into numerous cases. This task seems very suitable for automation, especially with the help of modern technology.
This time, Tao used ChatGPT as his AI tool. After about four hours of programming, with frequent assistance from the large model, he successfully created a proof-of-concept tool.
Meanwhile, Tao also shared his conversation process with ChatGPT, which was quite lengthy.
Link: https://chatgpt.com/share/68143a97-9424-800e-b43a-ea9690485bd8
From the beginning, Tao presented his requirements to ChatGPT: "I want to write some Python classes to manipulate symbolic expressions. And I want a class to represent variables like x, y, z... Can you help me write some basic classes to get started?"
ChatGPT thought for 6 seconds and provided an answer.
After completing this step, the next round of dialogue began, with Tao asking, "I see you implemented + operation with add, that's great. So what are the corresponding methods for * and / ?"
ChatGPT also provided an answer:
Throughout the process, Tao continuously asked questions, and ChatGPT answered everything, whether simple or complex problems:
"How to import a Python file in the same directory as the current Python file?"
Finally, with ChatGPT's strong assistance, Tao completed this proof-of-concept software tool.
Among many renowned mathematicians, Tao is one of the earlier ones to accept and discover the mathematical value of large AI models like ChatGPT. He once predicted that "if used properly, by 2026, AI will become a trustworthy co-author in mathematical research and many other fields."
Tao has used large models for research multiple times. He successfully solved a mathematical proof problem with GPT-4's help (GPT-4 proposed 8 methods, with 1 successfully solving the problem), and even discovered a hidden bug in his own paper with AI's assistance.
Tao also suggests that if anyone wants to develop such software, it's best for mathematicians and professional programmers to collaborate to complement each other's strengths.
"This is certainly an extremely inelegant proof, but elegance is not the point; the point is that it is automated."
Looking back at the entire process, we can draw inspiration from Tao's experience that our use of large models may just be the tip of the iceberg, with more functions waiting to be unlocked.
Reference links:
https://terrytao.wordpress.com/2025/05/01/a-proof-of-concept-tool-to-verify-estimates/
This article is from the WeChat public account "Machine Heart", editors: Egg Sauce, Chen Chen, published by 36Kr with authorization.
