Исследователи из Google DeepMind и Кембриджского университета представили систему на базе Gemini, способную самостоятельно находить и доказывать математические закономерности для машин Тьюринга. Работа сосредоточена на задаче Busy Beaver для машин с шестью состояниями и двумя символами.
Агентная система анализирует результаты симуляций, выявляет повторяющиеся структуры и формулирует математические правила. Корректность доказательств проверяется в среде Lean 4, что позволяет строго подтвердить математические рассуждения без участия человека.
Система вывела и формально подтвердила правила для 11 машин класса BB(6), которые ранее не были проанализированы. Эти закономерности позволяют описывать множество шагов вычислений через арифметические преобразования, что напоминает структуру гипотезы Коллатца.
Команда также получила новые способы анализа или доказательства для 15 машин, ранее изученных математиками. Несмотря на успех, вопрос об остановке этих 11 машин остается открытым, так как найденные правила не гарантируют завершение вычислений.
Авторы предлагают классифицировать такие экземпляры как Cryptids — машины с описанным поведением, но неясным статусом остановки. В дальнейшем исследователи планируют расширить метод на другие виды вычислительных задач, выходя за рамки текущих ограничений.
