Проект Star Fleet Math на GPT-5.6 решил две задачи Эрдёша с помощью до 20 параллельных агентов

Американский разработчик Колин Снайдер вместе с консультантом Майком Кимом опубликовал проект Star Fleet Math, Mac-приложение, которое пытается доказывать открытые математические задачи из списка Пола Эрдёша (сайт erdosproblems.com). Идея выросла из более раннего проекта «Игнис», который Снайдер делал вместе с Дхрувом Агарвалом и Нитином Кесарвани в New Turing Institute.

Приложение управляет до 20 параллельными агентами, на языке проекта «звездолётами»: каждый работает над отдельной задачей на выделенном сервере с 60 виртуальными ядрами (vCPU) и собственным инстансом модели GPT-5.6. Всё написано с нуля на TypeScript и среде выполнения Bun.

У каждого агента в распоряжении, вычислительные всплески до 2000 vCPU для перебора, который дробится на тысячи независимых однопоточных задач, и всплески GPU H100 для массово-параллельного перебора. Для поиска математических фактов есть база лемм и теорем на языке формальных доказательств Lean 4, по словам авторов, крупнейшая в мире, с поиском на обычном английском через эмбеддинги gemini-embeddings-2 и векторную базу Chroma, а также индекс препринтов arXiv.org и репозиториев GitHub, построенный через Firecrawl.dev. Присланные доказательства проверяет отдельный агент-верификатор на базе Claude Fable; после того как Fable одобрит доказательство, Снайдеру приходит сообщение в iMessage для финальной проверки. Каждая подтверждённая лемма или теорема попадает в локальную систему долгосрочной памяти Ton 618 и вплетается в общий граф зависимостей, поэтому новые доказательства опираются на уже проверенные. Наконец, у агента есть отдельная песочница на 60 vCPU и 120 ГиБ памяти с предустановленными SAT/SMT-решателями (CaDiCaL, kissat, Z3), решателем CP-SAT от Google, системами компьютерной алгебры (SageMath, PARI/GP, GAP, Macaulay2) и полными наборами инструментов Rust, CUDA C++ и Lean 4.

Авторы подчёркивают, что сознательно отбирали только задачи без опубликованных частичных или неформальных решений в интернете, чтобы не «переоткрывать» уже известные ответы. На сайте выложены материалы по 27 предложенным решениям (в заголовке обсуждения на Hacker News фигурирует «20 задач», возможно, более ранний или округлённый счётчик; на момент подготовки материала на сайте заявлено 27). Полностью, с разбором математики, показаны два случая.

Задача Эрдёша №123 (теория чисел, приз $250) спрашивает: для трёх попарно взаимно простых целых чисел a, b, c больше единицы, будет ли каждое достаточно большое целое число суммой различных чисел вида a^i · b^j · c^k, ни одно из которых не делит другое? Ответ, который проект доказал и полностью формализовал в Lean 4, да: для любой такой тройки это верно начиная с некоторого порога. Сложность была не в самой сумме, а в требовании «ни одно слагаемое не делит другое»: обычные схемы индукции используют числа разных масштабов, а такие числа, наоборот, склонны делить друг друга; при этом «неделимые» подмножества чисел оказываются слишком редкими, чтобы покрыть все числа подряд. Прежние попытки застревали на проблеме «конечного зерна»: сначала требовалось покрыть широкий, в мультипликативном смысле, стартовый интервал, а имевшиеся техники, арифметические прогрессии Ван дер Вардена и Хейлса, Джуэтта, готовые тождества, полные системы вычетов, давали длинные последовательности решений, но не давали контроля над нижней границей этого интервала. Прорыв, работать на одном «однородном» уровне показателей степени, где любые слагаемые автоматически оказываются взаимно неделимыми; строить на этом уровне длинные арифметические прогрессии через конструкцию с «рёберными кодами» и теорему Хейлса, Джуэтта из библиотеки Mathlib; а затем добавить необязательный «внутренний слой», запасные слагаемые в контролируемом мультипликативном окне, которые можно по желанию включать в сумму, не сдвигая нижнюю границу интервала. Это позволяет расширять доказанный интервал сколь угодно широко и снимает проблему «конечного зерна», а вместе с ней завершает доказательство сразу для всех шести возможных порядков тройки чисел. Формальная проверка показывает: проект на Lean 4 и Mathlib собирается целиком, поиск по исходному коду не находит заглушек «sorry», а итоговая теорема зависит только от трёх стандартных для Lean аксиом (propext, Classical.choice, Quot.sound), то есть без скрытых недоказанных допущений. Отдельно авторы отмечают: формулировка задачи ровно в том виде, как она дословно написана на сайте Эрдёша, ложна в одном вырожденном граничном случае; проект фиксирует это отдельно и доказывает содержательную, неформально подразумеваемую версию гипотезы, ту, которой реально пользуются в литературе.

Задача Эрдёша №129 (теория Рамсея) определяет R(n;3,r), наименьшее число вершин N, такое что при любой раскраске рёбер полного графа на N вершинах в r цветов найдётся набор из n вершин, среди которых хотя бы один цвет не образует треугольника. Источник 1997 года, на котором основана задача, предполагал оценку R(n;3,r) < C(r)^√n для некоторой константы C(r). У формулировки была запутанная судьба: математик Антониу Жирау уже показывал, что дословное прочтение оценки ложно, но в базе задач Эрдёша пункт всё равно числился «открытым», потому что было неясно, не имел ли автор 1997 года в виду что-то другое, а простое опровержение буквальной фразы не закрывало бы содержательный вопрос. Проект формально доказал в Lean 4, что для двух цветов (r = 2) при всех n ≥ 120 выполняется 2^⌊n/120⌋ < R(n;3,2) ≤ 2^(2n), то есть рост R(n;3,2) экспоненциален по n, и никакая константа C > 1 не может обеспечить более медленный рост вида C^√n сразу для всех n. Это одновременно опровергает буквальную формулировку 1997 года и снимает прежнюю двусмысленность, она ложна по существу, а не из-за неточной передачи текста. Ключевым в доказательстве, судя по доступному тексту, стало вероятностное рассуждение о рёберно-непересекающихся треугольниках внутри проверяемых наборов вершин, на этом месте исходный материал обрывается.

Для каждой опубликованной задачи проект выкладывает пакет для независимой проверки: исходную формулировку, формальное утверждение на Lean 4, весь закреплённый Lean-проект и скрипт-верификатор с пошаговой инструкцией для ИИ-агента читателя. По словам авторов, проверка занимает около 20 минут, большая часть которых уходит на скачивание библиотеки Mathlib.

Ключевые факты

Колин Снайдер (при участии Майка Кима) выпустил Star Fleet Math, Mac-приложение, которое управляет до 20 параллельными агентами («звездолётами»); каждый работает на выделенном сервере с 60 vCPU и собственным инстансом GPT-5.6
У каждого агента есть вычислительные всплески до 2000 vCPU и GPU H100, поиск по базе лемм Lean 4 через эмбеддинги gemini-embeddings-2, индекс arXiv.org и GitHub через Firecrawl.dev, верификатор на Claude Fable и песочница с решателями Z3, CaDiCaL, kissat, CP-SAT и системами SageMath, PARI/GP, GAP, Macaulay2
На сайте заявлено 27 предложенных решений открытых задач Эрдёша; авторы намеренно отбирали только задачи без уже опубликованных частичных решений
Задача Эрдёша №123 (теория чисел, приз $250) доказана и полностью формализована в Lean 4: сборка проходит без заглушек «sorry», доказательство опирается только на три стандартные аксиомы Lean
Задача Эрдёша №129 (теория Рамсея): предложенную в 1997 году оценку R(n;3,2) < C^√n формально опровергли, доказав 2^⌊n/120⌋ < R(n;3,2) ≤ 2^(2n), экспоненциальный рост

Почему это важно

ИИ-агенты всё активнее пробуют силы не только в написании кода, но и в математических исследованиях, и здесь, проверяемый, а не рекламный пример: не результат бенчмарка, а две задачи из известного списка открытых проблем Пола Эрдёша, закрытые с доказательством, которое проверяет компьютер, а не только языковая модель. Формальная система Lean 4 не примет доказательство с логическим пробелом, итог либо компилируется целиком, либо нет, и это не сводится к «модель так сказала». Проект также показывает, что такую проверку можно поставить на поток: до 20 агентов одновременно, каждый со своим сервером, вычислительными всплесками и набором инструментов, а не разовое ручное доказательство одной задачи.

Кому это важно

Математикам и энтузиастам, которые следят за списком задач Эрдёша (erdosproblems.com), закрыты ещё два пункта, причём по задаче №129 снята многолетняя двусмысленность, на которую раньше указывал Антониу Жирау. Сообществу формальной математики вокруг Lean 4 и Mathlib, проект показывает рабочий пример поиска и переиспользования лемм в большом масштабе через эмбеддинги и накопления проверенных результатов в собственном графе зависимостей (Ton 618), на который опираются следующие доказательства. Разработчикам агентных систем, это готовая архитектура «агента с полным арсеналом»: собственные вычислительные всплески, песочница с классическими солверами, индексы внешних источников, второй ИИ в роли верификатора и постоянная память. Наконец, это живой кейс использования для инструментов из стека, GPT-5.6 от OpenAI, Claude Fable от Anthropic, Firecrawl.dev и решателей Google.

Как это применить

Для каждой заявленной задачи на сайте лежит пакет для самостоятельной проверки: исходная формулировка, формальное утверждение на Lean 4, весь закреплённый Lean-проект и скрипт-верификатор с пошаговой инструкцией для собственного ИИ-агента читателя. По словам авторов, проверка занимает около 20 минут, большая часть которых уходит на скачивание библиотеки Mathlib. То есть результат, не голословное заявление: имея инструментарий Lean (или агента, способного им управлять), можно перепроверить доказательство самостоятельно, а не верить пересказу на слово. Готового публичного сервиса или API здесь нет, это Mac-приложение и отчёт одного разработчика, а не выпущенный продукт, поэтому практическая польза для стороннего читателя, прежде всего сам рецепт проверки и архитектура, а не инструмент, который можно поставить уже сегодня.

Можно ли доверять

В пользу доверия, полная формализация в Lean 4 для обеих разобранных задач: проект собирается целиком, заглушек «sorry» нет, а доказательство опирается только на три стандартные для Lean аксиомы (propext, Classical.choice, Quot.sound), то есть без скрытых недоказанных допущений. Авторы также аккуратно обходят классическую ловушку: по задаче №123 отдельно отмечают, что формулировка в буквальном виде ложна в вырожденном граничном случае, и доказывают именно тот, неформально подразумеваемый, вариант гипотезы, которым реально пользуются в литературе; по задаче №129 явно разбирают, а не обходят стороной, двусмысленность в формулировке 1997 года. Есть и человеческий контроль: после одобрения ИИ-верификатора Claude Fable автору приходит сообщение в iMessage для финальной проверки. Из оговорок: это самостоятельная публикация на сайте разработчика, без внешнего рецензирования и подтверждения от кураторов списка Эрдёша; заявлено 27 предложенных решений, но в доступном тексте источника полностью разобраны только два, по остальным независимо проверить нечего. Формулировка на сайте, именно «предложенное решение», не более сильный статус.

Риски и подводные камни

Формальная проверка в Lean 4 гарантирует только то, что доказательство соответствует формальной формулировке в том виде, в каком её записали, но сама по себе не гарантирует, что эта формулировка верно передаёт смысл исходной, неформальной задачи Эрдёша: это классический риск разрыва между формализацией и содержанием. Проект явно осознаёт эту ловушку и аккуратно разбирает её в двух показанных случаях, но ту же аккуратность нужно повторить отдельно для каждого из ещё 25 заявленных решений. Подход прожорлив по вычислениям, всплески до 2000 vCPU, GPU H100, 20 одновременно работающих агентов по 60 vCPU и 120 ГиБ памяти каждый, поэтому распространить его на остальные задачи списка, вопрос не только программного кода, но и бюджета на инфраструктуру. Наконец, конвейер завязан на конкретную закрытую модель GPT-5.6 и конкретный верификатор Claude Fable, воспроизводимость результатов зависит от доступа к обоим.

«Многие задачи со статусом «открытая» уже имеют в интернете неформальные или частичные ответы, мы изо всех сил старались не браться ни за одну из них.»

— Колин Снайдер, автор Star Fleet Math