AI Science
Открытая задача Эрдёша получила полностью автономное доказательство с формализацией в Lean
В научной подборке сегодня один, но очень сильный результат: авторы arXiv-работы утверждают, что система Aristotle впервые полностью автономно решила открытую задачу из списка Эрдёша, а затем оформила доказательство в Lean. Если вывод выдержит проверку, это будет важный шаг от олимпиадных и тестовых задач к настоящему математическому исследованию с машинной верификацией.