Решённая задача ещё не открытие: Тао предлагает оценивать ИИ по новым идеям

Математик Теренс Тао предлагает оценивать автоматические решения по тому, какие новые идеи они дают и что объясняют о сложности соседних задач. По его оценке, ответ без такого разбора может иметь ничтожную или отрицательную ценность. Дефицитом становится поиск плодотворной задачи. Даже слух о работе над ней способен вызвать массовые попытки решить её с помощью ИИ раньше авторов, считает Тао. Это ослабляет стимул открыто делиться направлениями исследования. [Тао объясняет, почему одних ответов недостаточно](https://teorth.github.io/tao-web/ai-views.html).

Доказательство и понимание. Участники Equational Theories Project определили все 22 млн отношений следования между 4694 законами: какие утверждения следуют из других, а какие нет. Они объединили человеческие и автоматические доказательства и проверили их в Lean, системе формальной проверки математики. Результат зафиксирован в версии статьи от 16 декабря 2025 года. [Участники описали полную проверку отношений между законами](https://arxiv.org/abs/2512.07087).

Сначала участники изобрели методы построения бесконечных контрпримеров, опровергающих предполагаемые связи между законами. Позднее для части задач нашлись малые конечные контрпримеры. Тао отмечает, что ранний автоматический ответ мог бы лишить исследователей повода искать более содержательный метод.

Предсказать, какие задачи уже посильны ИИ, тоже трудно. Тао связывает это с быстрым развитием моделей и тем, что компании не публикуют неудачные попытки и процесс решения. [Тао разбирает пример Equational Theories Project и неопределённость возможностей моделей](https://teorth.github.io/tao-web/ai-views.html).

От ответа к гипотезе. В продолжении работы над задачей Эрдёша №1026 Тао за 1 час работы AlphaEvolve получил оценки для значений n от 1 до 16. Найденная закономерность помогла ему и Алексееву сформулировать следующую гипотезу. В этом случае автоматический поиск дал материал для дальнейшего исследования. [Тао описал работу с Aristotle и AlphaEvolve 8 декабря 2025 года](https://terrytao.wordpress.com/2025/12/08/the-story-of-erdos-problem-126/).

Материалы Equational Theories Project доступны для самостоятельного изучения: код, документация и Equation Explorer для просмотра связей между законами. После установки Lean и клонирования репозитория локальная сборка выполняется тремя командами.

```sh cd equational_theories/ lake exe cache get lake build ```

[Код, Equation Explorer и инструкция сборки доступны на сайте проекта](https://teorth.github.io/equational_theories/).

Тао предлагает компаниям соревноваться за первую новую математическую идею, а не за первый ответ.