«Математический сверхинтеллект» Aristotle решил 30-летнюю задачу Эрдёша
habr.comИИ-система Aristotle от стартапа Harmonic впервые полностью автономно решила открытую математическую задачу. На решение задачи Эрдёша #124, сформулированной в 1995–1997 годах, ушло 6 часов.
Еще минута понадобилась на формальную верификацию доказательства в системе Lean. Человек участвовал только в постановке задачи.Harmonic развивает концепцию "математического сверхинтеллекта" (MSI) — ИИ, который работает с формальным языком Lean4 и автоматически верифицирует свои доказательства, что исключает "галлюцинации".
Сократили операционную рутину и расходы. Пять проблем, которые решает All-in-One HRM-платформа HURMA
