" Стартап Harmonic, основанный CEO Robinhood Владом Теневым, объявил, что их ИИ Aristotle самостоятельно доказала проблему Эрдёша №124 в формальной системе Lean Prover. Ранее этот ИИ получил золото на олимпиаде по математике.
Как Aristotle справился?
Борис Алексеев, математик-исследователь, протестировал бета-версию Aristotle. За 6 часов Aristotle сгенерировал доказательство в Lean Prover, а проверка заняла минуту. ИИ в том числе исправил опечатку в формальной формулировке из проекта Formal Conjectures, сделав задачу чуть сложнее.
Математическое сообщество сказало, что Aristotle решил легкую версию, а не сложную задачу из BEGL96. Это хорошее решение для ИИ, хотя в ретроспективе очень простое. Математик Томас Блум предлагает оставить задачу Эрдеша №124 открытой, а решённую версию ИИ вынести в связанные проблемы.
А в соцсетях люди пишут, что работа ИИ на уровне олимпиады по математике. Возможно, была утечка из тренировочных данных, похоже на олимпиадные задачи. Но сообщество оценило автоматизацию, ИИ генерирует Lean-пруфы без присмотра — это круто.
