AI Radar
Исследователи Tencent с помощью научного агента Hyra построили семейство конечных множеств, которое разрешает давний вопрос о соотношении роста сумм и разностей. Агент предложил расширяемую конструкцию, люди оформили строгий вывод, а доказательство дополнительно проверили в Lean 4.
Задача относится к аддитивной комбинаторике. Для конечного множества целых чисел A рассматриваются множество всех попарных сумм A+A и множество разностей A−A. Их относительный рост задают величины σ(A)=|A+A|/|A| и δ(A)=|A−A|/|A|, а отношение C(A)=log σ(A)/log δ(A) показывает, насколько быстро суммы расширяются по сравнению с разностями. Теория даёт верхнюю границу C(A)≤2, но более полувека оставалось неясно, можно ли подойти к двойке сколь угодно близко или это лишь заведомо неточная оценка.
Предыдущие работы постепенно улучшали отдельные примеры: около 1,0290 в 1969 году, 1,0598 в 1973-м и 1,1259 в 2013-м. Недавний поиск с участием ИИ поднял результат до 1,1449, а описанный в новой работе внутренний эксперимент с Codex на базе GPT-5.5 и человеческими подсказками — до 1,2851. Однако рекордное конечное множество само по себе не отвечает на вопрос о пределе. Для этого требовалось не очередное удачное расположение чисел, а параметризованное семейство, которое можно увеличивать без потери нужного свойства.
Сначала Hyra тоже оптимизировала конечные наборы и улучшила известный ориентир примерно с 1,14 до 1,21. Дальнейшему перебору мешали расход памяти и быстро растущая вычислительная сложность, а найденные численные конфигурации плохо переводились в доказательство. Тогда агенту поручили искать уже математическую конструкцию и рассуждение, используя LLM-судью для обратной связи по ходу исследования. Примерно через 24 часа Hyra предложила основу решения: двенадцатеричную структуру для контроля размера множества разностей, симметричный аддитивный базис в циклической группе и китайскую теорему об остатках для ускоренного роста множества сумм.
Из этой идеи исследователи получили семейство конечных множеств A_K и доказали, что при увеличении параметра K значение C(A_K) стремится к 2. Следовательно, двойка действительно является точной верхней гранью, хотя никакое отдельное конечное множество её не достигает. Роль Hyra здесь выходит за пределы автоматического перебора: агент помог перейти от улучшения численного рекорда к общему шаблону, который допускает строгий математический анализ.
Работа выполнена с исследовательским агентом Hyra, представленным Tencent Hunyuan 21 июля и основанным на модели Hy3 с 295 млрд параметров, из которых активируются 21 млрд. После появления кандидатной идеи математики самостоятельно проверили рассуждение, восстановили полный строгий вывод и опубликовали формализацию в Lean 4. Это важная страховка от правдоподобных, но неверных переходов языковой модели. При этом результат пока размещён только как препринт на arXiv и ещё не прошёл независимое рецензирование.
Этот случай показывает практичную схему применения ИИ в математике: агент исследует пространство примеров и предлагает обобщаемую конструкцию, специалисты превращают её в доказательство, а формальная система проверяет логические шаги. Формализация делает результат значительно проверяемее обычного ответа модели, но статус препринта всё равно требует независимой экспертизы математического сообщества.
DSML editors review the selection. AI helps deduplicate signals and draft the text; the published edition remains an editorial product, not a feed of individual channels.
