Исследователи из Google DeepMind и Кембриджского университета применили агентную систему на базе Gemini для изучения задачи Busy Beaver BB(6). Команда проанализировала 1094 машины Тьюринга с шестью состояниями, отобрав 52 из них для детального исследования.
Система разработала и формально верифицировала правила ускорения для 11 ранее не изученных машин. Эти правила описывают поведение систем без пошаговой симуляции, однако они не дают ответа на вопрос, завершают ли машины работу.
Процесс включал симуляции, создание гипотез и построение доказательств в системе Lean 4. Такой подход гарантирует логическую корректность выводов, не зависящую от доверия к самой нейросети.
Результаты работы опубликованы в препринте на arXiv 15 октября 2026 года под идентификатором 2610.22603. В состав исследовательской группы вошли Марко Дос Сантос, Том Захави и Вивек Вирия.
