9 января стартап Harmonic объявил об отмене листа ожидания для своей системы Aristotle — теперь любой желающий может зарегистрироваться на сайте и сразу получить доступ к API. Aristotle — это система автоматического доказательства теорем, которая в июле 2025 года решила 5 из 6 задач Международной математической олимпиады (IMO), показав результат на уровне золотой медали. В отличие от аналогичных моделей OpenAI и Google DeepMind, которые достигли того же уровня, но остаются закрытыми, Aristotle стал первым публично доступным ИИ такого класса с формальной верификацией.

Ключевая особенность Aristotle — каждое решение формализуется в языке доказательств Lean 4, и если код успешно проходит проверку компилятора, то решение считается формально верифицированным. По словам CEO Harmonic Тюдора Ачима, это позволяет гарантировать отсутствие галлюцинаций в поддерживаемых доменах — количественных и математических задачах. Такой же подход используется для верификации в авиации и медицинском оборудовании. Помимо олимпиадных задач, связка GPT-5.2 и Aristotle решила задачу Эрдёша #728 — открытую проблему о делимости факториалов 1975 года. Доказательство формализовано в Lean и признано Теренсом Тао. На бенчмарке верификации кода VERINA Aristotle показал результат 96,8%.

Система работает через CLI-интерфейс: пользователь устанавливает Python-библиотеку aristotlelib, получает API-ключ и запускает интерактивный терминал. Задачи можно формулировать как на языке Lean 4, так и на обычном английском — модель сама транслирует запрос в формальное представление. Архитектура Aristotle включает три компонента: поисковую систему доказательств на базе трансформера с более чем 200 миллиардами параметров, модуль генерации и формализации лемм, а также специализированный решатель геометрических задач Yuclid.

Harmonic основан в 2023 году, среди сооснователей — Влад Тенев, CEO Robinhood. В ноябре 2025 года стартап привлек $120 млн в раунде Series C при оценке $1,45 млрд. На сегодня Aristotle — единственный публично доступный ИИ уровня золотой медали IMO с формальной верификацией: аналогичные модели OpenAI и Google DeepMind закрыты.

P.S. Поддержать меня можно подпиской на канал "сбежавшая нейросеть", где я рассказываю про ИИ с творческой стороны.