ИИ-агент Tencent Hyra решил задачу, с которой не справились AlphaEvolve, GPT и Claude

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

Формальная проверка доказательства выложена в открытый репозиторий на Lean 4 — языке для машинной верификации математических утверждений. Это показывает, что открытые ИИ-агенты способны решать сложные математические проблемы, которые остаются непосильными для закрытых моделей ведущих лабораторий.