Агентный пайплайн на базе Gemini автономно обнаружил и формально проверил в Lean новые ускорения для 11 машин Busy Beaver (BB(6))
В препринте arXiv:2610.22603v1 описан агентный пайплайн на базе Gemini, объединяющий распознавание паттернов, автоматическую генерацию гипотез, неформальное рассуждение и формальное доказательство в Lean для автономного поиска компактных, похожих на Коллатца ускорений шагов исполнения машин Тьюринга. Система нашла и формально проверила новые ускорения для одиннадцати машин BB(6), которые авторы предварительно пометили как «Cryptids» — машины с точными компактными описаниями, но с нерешённым вопросом останова.