Исследователи FAIR в Meta и Нью-Йоркского университета обучили 27-миллиардную модель отбирать математические утверждения по измеримой «интересности»: короткая формулировка должна требовать сложного доказательства. В препринте от 23 сентября система генерирует формальные теоремы, пытается их доказать и ранжирует доказанные кандидаты — без заранее заданного человеком списка целей.

Авторы определили «интересность» как отношение предсказанной сложности доказательства к длине описания утверждения. Для оценки сложности они дообучили Qwen3.6-27B примерно на 100 тысячах примеров из формальной библиотеки Mathlib. По результатам самих исследователей, специализированная модель справилась с этой оценкой точнее универсальных передовых моделей.

После оптимизации по новой метрике доля сгенерированных утверждений, которые существенно или полностью повторяли содержимое Mathlib, снизилась с 91,9% до 30,6%. В отдельном опыте система итеративно расширяла небольшую формальную библиотеку: новые доказанные теоремы становились основой для следующего раунда генерации и отбора.

Главное ограничение спрятано в самом слове «интересность». Здесь это операционная метрика, а не оценка математиков: короткое утверждение с длинным доказательством не обязательно окажется важным или полезным для дальнейших исследований. Работа пока существует как препринт, независимо не воспроизведена и проверяет метод внутри формальной среды Mathlib. Поэтому результат показывает способ сортировать машинные гипотезы, но не доказывает, что ИИ уже способен самостоятельно выбирать крупные направления математики.