Google научили ИИ-агентов находить новые квантовые алгоритмы и сразу доказывать их корректность и стоимость в Lean. Над этим работала как команда DeepMind, так и Quantum. Эта работа отличается от прошлых подходов, где ИИ-агенты проверяли квантовые схемы численным моделированием на классическом компьютере. Здесь же агенты работают с алгоритмами на тысячах кубитов, которые невозможно просимулировать классически, но при этом корректность гарантируется математическим доказательством, а не тестами. Интересно, что на 5 задачах, включая термоядерный синтез, фотохимию, ИИ нашёл схемы в 2.5–11 раз эффективнее лучших опубликованных решений, причём на тысячах кубитов там, где классическая проверка в принципе невозможна.