Tencent's scientific research agent has solved 50 years of unsolved mathematical problems, Yao Shunyu announced that he is recruiting people

Zhidongxi Author | Eggplant Editor | Cheng Qian Zhidongzhi reported on July 31 that yesterday, Tencent's chief AI scientist Yao Shunyu forwarded a paper by Tencent Hunyuan and shouted: "Hy AI4S is hiring :)", openly recruiting talents in the direction of AI for Science. On July 29, a paper involving Hyra, Tencent's Hunyuan scientific research agent, to solve mathematical problems was published on arXiv. Relying on Hyra's powerful deduction and exploration capabilities, Tencent's research team has made key progress and solved an open problem in the field of additive combinatorics that has lasted for more than 50 years. In Yao Shunyu's comment area, a netizen said that Hyra/Hy3's paper was "too crazy". It used explicit construction to solve a decades-old unsolved sum set problem. He never expected that this would appear in a recruitment post. Some people also wonder: "Will the next Fields Medal winner be AI?" It is worth noting that this afternoon, Tencent's recruitment platform also announced the recruitment of the AI ​​Infra team led by Yao Shunyu. On July 21, Tencent Hunyuan launched the scientific research intelligent body Hyra. It is based on the Hy3 model, which was open sourced this month, with a total parameter volume of 295 billion and an activation parameter volume of 21 billion. Hyra is responsible for automating exploration work when solving this problem and helping researchers explore potential mathematical construction ideas. Hyra first optimized the existing finite set cases through search, and then further proposed a parameterized construction plan that can be infinitely expanded: relying on the hexadecimal structure to constrain the size of the difference set, combined with the symmetric addition basis of the cyclic group and the Chinese remainder theorem, to achieve faster expansion of the sum set. After the AI ​​outputs the candidate direction, the researchers verify the ideas, derive a complete and rigorous proof, and complete formal verification with the help of Lean4. This additive combinatorics problem studies the relationship between the scale expansion of integer sets after addition and subtraction operations. For example, given a finite set of integers A, by adding any two elements in the set and removing duplicate results, you can get the "sum set" A+A; similarly, by subtracting any two elements, you can get the "difference set" A-A. mathematician