There is a version of the AI-and-mathematics story that goes like this:
Give the model a difficult problem. The model thinks very hard. The model produces a proof. Mathematicians become unemployed and take up gardening.
Reality, fortunately, is becoming considerably more interesting.
A new paper by Haowei Lin and Shanda Li, “Settling the Optimal Exponent Relating Sumsets and Difference Sets,” resolves a combinatorics problem whose relevant bound dates back more than half a century. And the discovery was developed with the assistance of Hyra, Tencent’s AI research agent powered by the open-weights Hy3 model. (arXiv)
The result itself is interesting mathematics. But I think the workflow that produced it may be even more important.
A 50-Year-Old Question About Sums and Differences
Take a finite set of integers A. From it, construct two new sets:
A + A: every number you can obtain by adding two elements of A.
A − A: every number you can obtain by subtracting one element from another.
Mathematicians measure how much these operations expand the original set using two quantities:
and
Classical sum-difference inequalities relate the two:
The exponent 2 on the upper side was already known to be optimal. The annoying unresolved question was the other direction.
Could the exponent 1/2 be improved? Equivalently, could one construct sets where the logarithmic relationship between sumset growth and difference-set growth gets arbitrarily close to 2?
For more than fifty years, nobody had a construction proving that it could. Now there is one. (arXiv)
Enter Hyra
This is where the story becomes much more interesting than another benchmark score. According to the paper, Hyra assisted the researchers in developing both the construction and its proof. The agent is built around Tencent’s open-weights Hy3 model, a 295B-parameter mixture-of-experts model with 21B parameters active per token. (arXiv)
Rather than merely being asked: “Please solve this 50-year-old theorem.” the agent could participate in the exploratory process.
Search. Generate candidate constructions. Test mathematical behavior. Look for patterns. Discard failures. Refine promising structures. And eventually help expose the core construction from which a general proof could be developed.
This distinction matters enormously. The interesting capability isn’t answering mathematics questions. It’s participating in mathematical research.
Search Is Part of Intelligence
Humans sometimes romanticize mathematical discovery as a sequence of brilliant insights appearing mysteriously in someone’s head.
There is obviously insight involved. There is also an enormous amount of search. Try this construction. No.
Change this parameter. Still no. Look at small cases. Interesting. Generalize. Break it. Try again.
Repeat this for several months.
Machines have a rather obvious advantage in the less glamorous part of that process: they don’t get bored.
Give an agent a well-defined search environment, enough compute and a way to evaluate progress, and it can explore an absurd number of possibilities while the human mathematician does something machines remain notoriously bad at: deciding what the result means. That combination is beginning to look powerful.
The Result
Lin and Li construct an explicit family of finite sets
subset
for which
That settles the question. The 1/2 exponent in the classical lower sum-difference inequality cannot be improved. It is optimal. (arXiv)
What had remained unresolved for decades now has an explicit construction and proof. And the paper doesn’t hide the role of AI somewhere in an acknowledgements paragraph.
The abstract itself states that the construction and proof were developed with Hyra’s assistance. (arXiv) I like this.
If AI is becoming part of scientific methodology, its contribution should be documented like any other important computational tool.
Then Another AI Entered the Room
The story doesn’t end with discovery.
The result was also formalized in Lean 4, turning the mathematical argument into something that can be checked mechanically.
The public repository contains the formalization across multiple Lean files covering the construction, quantitative results, limits and main theorem. (GitHub) Explore the formal proof repository
This creates a particularly interesting research pipeline:
AI-assisted exploration → human mathematical interpretation → conventional proof → formal verification
That may prove much more consequential than models simply generating papers. Because one of the obvious problems with AI-generated mathematics is verification.
Generating candidate mathematics can become extremely cheap. Human mathematical attention cannot.
We’ve already seen Terence Tao warning about precisely this emerging imbalance: if proof production accelerates dramatically while exposition, review and community absorption remain human-speed processes, mathematics develops a verification bottleneck.
Formal methods provide one possible escape route. The same AI ecosystem that generates candidate discoveries may increasingly help translate them into machine-verifiable mathematics.
This Is What AI for Science May Actually Look Like
I don’t think the important conclusion is: “Hy3 is better than mathematicians.” That’s both premature and rather boring. The interesting part is the division of labor.
The agent can search an enormous combinatorial space. The mathematicians can recognize structure, correct mistakes, determine significance and transform the discovered pattern into mathematics worth publishing.
Formal verification can then provide another layer of confidence. Different systems are good at different parts of the epistemic pipeline. That is considerably more realistic than waiting for a single artificial mathematician to emerge from a chatbot window wearing a Fields Medal.
Open Models Make This More Interesting
There is another detail worth noticing.
Hy3 is an open-weights model released under Apache 2.0. Tencent describes it as a 295B MoE with 21B active parameters and a 256K context window. (GitHub) That’s important because scientific research benefits enormously from reproducibility and controllability.
Researchers don’t necessarily want an opaque consumer chatbot that may silently change next Tuesday. They want models they can deploy, instrument, wrap in specialized agents, connect to tools and run repeatedly under controlled conditions.
The future of AI-assisted science may therefore depend at least as much on research harnesses around models as on the models themselves.
Hyra is an example of that direction. The model provides reasoning capability. The agent provides persistence, search, tools and workflow. The scientists provide the question, judgment and ultimately responsibility for the result.
The Scientist Isn’t Gone. The Search Budget Changed.
This is perhaps the part I find most important. For centuries, scientific progress has been constrained by human cognitive bandwidth. A researcher can explore only so many hypotheses. Read so many papers. Run so many calculations. Follow so many dead ends. AI agents change that constraint.
Not by magically replacing scientific judgment. By making search dramatically cheaper.
Imagine giving every mathematician a research agent capable of exploring candidate constructions continuously for 24 hours. Then a week. Then a month.
Now imagine thousands of researchers doing this simultaneously across mathematics, physics, biology and materials science. Most searches will produce nothing. Some will produce nonsense. A few may produce exactly the strange construction nobody thought to try. And that’s enough.
Final Thoughts
For years, we measured AI in mathematics using exams. Then Olympiad problems. Then research-level problems. Those benchmarks were useful because we needed to know whether models could reason mathematically at all. But this result points toward a more important question:
Can AI participate productively in the actual process of discovery? Here the answer appears to be yes, at least in a meaningful and carefully documented case. An AI research agent helped explore a problem that had resisted mathematicians for more than fifty years.
Humans converted the discovery into rigorous mathematics. The result was then formalized for machine verification. That’s not autonomous science. It may be something more useful. It’s a new scientific instrument. And unlike a microscope, this one can spend the night trying ideas.