Найти в Дзене
Нейрозона сегодня
24 подписчика

Aristotle: ИИ для доказательства теорем стал публично доступным

1
1 мин
9 января стартап Harmonic открыл доступ к своей системе Aristotle — ИИ для автоматического доказательства теорем. Любой желающий может зарегистрироваться на сайте и получить доступ к API. В июле 2025 года Aristotle успешно решил 5 из 6 задач Международной математической олимпиады (IMO), продемонстрировав уровень золотой медали. В отличие от закрытых моделей OpenAI и Google DeepMind, Aristotle стал первым публично доступным ИИ такого класса с формальной верификацией. Ключевая особенность системы — формализация каждого решения на языке доказательств Lean 4 с последующей проверкой компилятором. Это гарантирует отсутствие "галлюцинаций" в математических задачах. Aristotle в связке с GPT-5.2 решил задачу Эрдёша #728, доказательство которой признано Теренсом Тао. На бенчмарке VERINA система показала результат 96,8%. Система работает через CLI-интерфейс с использованием Python-библиотеки aristotlelib. Задачи можно формулировать как на Lean 4, так и на английском языке. Harmonic, основанный в

9 января стартап Harmonic открыл доступ к своей системе Aristotle — ИИ для автоматического доказательства теорем. Любой желающий может зарегистрироваться на сайте и получить доступ к API.

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

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

Система работает через CLI-интерфейс с использованием Python-библиотеки aristotlelib. Задачи можно формулировать как на Lean 4, так и на английском языке.

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

Ну что ж, теперь математики всего мира могут спокойно спать, зная, что у них есть новый коллега, который не только умнее, но и не требует кофе и выходных. Хотя, кто знает, может, скоро и ему понадобится отпуск на Марсе.