AI solved a 30-year math problem in just 6 hours. Terence Tao: ChatGPT and others failed.

Last night, the mathematics community was shaken! The AI mathematician "Aristotle" cracked a simplified version of a 30 - year - old problem in just 6 hours with a single click, earning high praise from Terence Tao. The era of Vibe proving in the mathematical field has arrived.

A 30 - year - old unsolved mathematical problem has finally been cracked!

The AI mathematician "Aristotle", developed by HarmonicMath, independently completed Erdős Problem #124 with 100% autonomy.

It took only 6 hours in the Lean proof system, and the verification only took 1 minute.

There was no human participation or assistance throughout the process. This moment can be regarded as the "moon landing" moment in the mathematical community.

Vlad Tenev, the founder of HarmonicMath, sighed, "The mathematical community is undergoing a major change. The era of vibe proof has arrived!"

Even Terence Tao, the Fields Medalist, highly praised the AI mathematician "Aristotle".

The era of AI discovering mathematics has officially begun.

A 30 - year - old problem has been cracked. AI has achieved it.

For a long time, the "problem list" of mathematician Erdős Pál has been like the Mount Everest of knowledge, testing the limits of humanity.

The rewards for those unsolved problems mostly range from dozens of dollars to tens of thousands of dollars.

Its symbolic meaning is far greater than its actual value, and it has become a spiritual medal for countless mathematicians.

For 30 years, Problem #124 (Erdős #124), proposed in the paper "Complete sequences of sets of integer powers", has remained unsolved.

The core of E124 is: Given k natural numbers d_i ≥ 2, if ∑ 1/(d_i - 1) ≥ 1, then for any natural number n, there always exist a_i such that n = ∑ a_i.

Moreover, each a_i, in the "digits" under d_i, is limited to {0, 1}.

Put simply, it essentially asks - under extreme constraints, can any large number always be represented in "binary" without being affected by the base?

This involves the deep waters of "combinatorial mathematics", and traditional methods have been stuck on the gcd condition and boundary cases.

Until last night, this wall collapsed.

The Harmonic team created a prototype of "mathematical super - intelligence" - Aristotle, which combines reinforcement learning, Monte Carlo tree search, and the Lean formal language.

After inputting the problem, it searched hundreds of millions of proof strategies and finally output a 100% verifiable theorem.

Mathematician Boris Alexeev said that this is his favorite among the three theorems output by AI:

theorem erdos_124 : ∀ k, ∀ d : Fin k → ℕ, (∀ i, 2 ≤ d i) → 1 ≤ ∑ i : Fin k, (1 : ℚ) / (d i - 1) → ∀ n, ∃ a : Fin k → ℕ, ∀ i, ((d i).digits (a i)).toFinset ⊆ {0, 1} ∧ n = ∑ i, a i

Address: https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos124.md

By the way, there are two different versions of the E124 problem, both proposed by Erdős.

Currently, the AI Aristotle has solved a relatively simple version.

In terms of time, Aristotle took 6 hours, while Lean only took 1 minute.

The maintainer of the Erdős problem website said that Aristotle's performance was the most impressive!

Both ChatGPT and Gemini failed.

Terence Tao commented on this, "As far as I know, the in - depth research tools of Gemini and ChatGPT have not found any new and valuable literature on this problem."

Gemini gave a simple observation: If the number 1 is excluded, then the gcd condition becomes necessary; it also explained the condition

and linked it to some parallel research on Cantor sets, especially the "Newhouse gap lemma".

However, it did not find new literature directly related to this problem.

ChatGPT largely relied on this webpage as the main authoritative source, such as citing Aristotle's proof, other papers cited on this page, and pages of related problems.

Therefore, no new information was obtained, but readers may find these AI - generated summaries quite interesting.

Terence Tao: AI is harvesting the low - hanging fruits in mathematics.

On mathstodon, Terence Tao also shared his years of experience -

He said that the current real situation is: Unsolved mathematical problems follow a "long - tail distribution", and AI automation "harvesting" is concentrated at the very end of the long tail.

There are a large number of problems that are actually relatively easy to prove or disprove, but due to the limited number of expert mathematicians who can actually invest in research, these problems have received little attention.

In other words, there are actually many accessible "low - hanging fruits" hidden in this "tail":

If there is a way to solve these problems automatically on a large scale, it may produce a considerable number of new mathematical results.

Last year, Terence Tao experienced a similar situation in the Equational Theories Project.

In this project, they faced 22 million possible implications in universal algebra. If done entirely by humans, it would definitely take a very long time.

So, they decided to start with a relatively "low - tech" automated method and solved most of them in just a few days.

Next, they continued to use more complex methods to tackle the stubborn difficulties that could not be solved in the previous rounds.

Finally, it took human mathematicians several months to solve the few remaining particularly stubborn ones.

Currently, the Erdős problem website has recorded 1108 problems that have appeared in at least one of Erdős' papers.

Among them, there are well - known difficult problems like E3, as well as a large number of more obscure and rarely - noticed problems, and even Erdős himself never revisited them.

In recent weeks, nearly ten "unsolved" labels on this website have suddenly disappeared. All were discovered through literature search with the help of AI -

Actually, these problems had already been solved by others.

Human mathematicians who are researching these problems also use AI tools and formal proof assistants in combination:

Some verify existing proofs in Lean, some generate integer sequence terms related to these problems, and some fill in the missing proof steps in an existing idea.

Recently, another type of "low - hanging fruit" within the scope of automated tools has been discovered - problems that have unexpectedly become easy to solve due to technical flaws in the description.

E124 is a typical example. The complete version of this problem is somewhat difficult and has appeared in three of Erdős' papers.

However, a key assumption was omitted in two of them, making this version actually a direct corollary of Brown's criterion.

No one noticed this until Boris Alexeev threw the problem to the automated tool Aristotle. Unexpectedly, the AI independently found the loophole within a few hours and completed the formal proof in Lean.

It can be seen that AI is lighting up the "dark forest" of mathematics.

As Terence Tao said, "Automated tools first clear the easiest problems, separate the truly difficult part, and allow human mathematicians to spend their energy on worthy things."

References:

https://www.erdosproblems.com/forum/thread/124#post-1892

https://x.com/SebastienBubeck/status/1994946303546331508?s=20

https://mathstodon.xyz/@tao/115639983683442577

https://x.com/thomasfbloom/status/1995094668879462466?s=20

This article is from the WeChat public account "New Intelligence Yuan". The author is New Intelligence Yuan, and the editor is Taozi. It is published by 36Kr with permission.