Открыт бесплатный API-доступ к Aristotle — ИИ-математику уровня золотой медали IMO

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 миллиардами параметров, модуль генерации и формализации лемм, а также