[Tencent's Open-Source Model Hy3 Solves Half-Century Mathematical Problem, Complete Proof Verified by Machine] According to monitoring by Beating, Tencent's research agent Hyra, utilizing its open-source model Hy3, assisted two researchers in solving a combinatorial mathematics problem that had remained unresolved for over 50 years. The problem was: How much faster can the 'sum set' of an integer set grow compared to its 'difference set'? The mathematical community had long proven that the related exponent cannot exceed 2, but it was unclear whether 2 was the optimal answer. Hyra directed Hy3 to first search for specific sets and then attempt to propose a general construction. Approximately 24 hours later, the AI discovered the core solution ultimately adopted in the paper. The researchers then verified, refined, and organized the proof, with GPT-5.6 Sol assisting in converting it into Lean 4 for verification. The final paper proved that the exponent can approach 2 infinitely closely, confirming that the upper bound of 2 is indeed the optimal answer. Although AI did not author the entire paper, the most critical construction was indeed found by Hy3. [Original Link]