На arXiv опубликован препринт работы Хаовэя Линя из Tencent Hunyuan и Шанды Ли из Университета Карнеги — Меллона, ставящий точку в вопросе аддитивной комбинаторики. Ключевую конструкцию для решения задачи предложил исследовательский агент Tencent Hyra, работающий на открытой модели Hy3. Формальная проверка доказательства выложена в открытый репозиторий на языке Lean 4.
Задача в аддитивной комбинаторике, на которой проверяли себя системы AlphaEvolve, GPT и Claude, была решена именно агентом Hyra.