Стартап Harmonic убрал лист ожидания для своей системы Aristotle. Теперь любой может зарегистрироваться на сайте и сразу получить доступ к API. Aristotle — это система автоматического доказательства теорем.
В июле 2025 года она решила 5 из 6 задач Международной математической олимпиады. Результат соответствует золотой медали IMO. OpenAI и Google DeepMind создали аналогичные модели с таким же уровнем. Но они остаются закрытыми. Aristotle стал первым публично доступным ИИ такого класса с формальной верификацией.
Узнать подробнее про клуб ShareAI
Главная особенность Aristotle — каждое решение формализуется в языке доказательств Lean 4. Если код успешно проходит проверку компилятора, решение считается формально верифицированным. CEO Harmonic Тюдор Ачим объясняет, что это позволяет гарантировать отсутствие галлюцинаций в поддерживаемых доменах. Речь идет о количественных и математических задачах. Такой же подход используется для верификации в авиации и медицинском оборудовании.
Помимо олимпиадных задач, связка GPT-5.2 и Aristotle решила задачу Эрдёша #728. Это открытая проблема о делимости факториалов 1975 года. Доказательство формализовано в Lean и признано Теренсом Тао. На бенчмарке верификации кода VERINA Aristotle показал результат 96,8%.
Система работает через интерфейс командной строки. Пользователь устанавливает Python-библиотеку aristotlelib и получает API-ключ. После этого можно запускать интерактивный терминал. Задачи формулируются как на языке Lean 4, так и на обычном английском. Модель сама транслирует запрос в формальное представление.
Архитектура Aristotle включает три компонента. Первый — поисковая система доказательств на базе трансформера. Она содержит более 200 млрд параметров. Второй — модуль генерации и формализации лемм. Третий — специализированный решатель геометрических задач Yuclid.
Harmonic основали в 2023 году. Среди сооснователей — Влад Тенев, CEO Robinhood. В ноябре 2025 года стартап привлек 120 млн долларов в раунде Series C. Оценка компании составила 1,45 млрд долларов.
На сегодня Aristotle — единственный публично доступный ИИ уровня золотой медали IMO с формальной верификацией. Аналогичные модели OpenAI и Google DeepMind остаются закрытыми для широкой публики. Harmonic делает ставку на открытость как конкурентное преимущество.
