Иногда для полноценной научной заметки достаточно одного результата — если он действительно меняет планку ожиданий от ИИ в науке. Именно такой случай сегодня в математике.
Resolution of Erdős Problem #728: a writeup of Aristotle's Lean proof
Авторы работы пишут, что система Aristotle автономно решила открытую задачу №728 из списка Эрдёша, после чего доказательство было формализовано в Lean. Если это утверждение подтвердится, речь идёт не просто о хорошем выступлении на бенчмарке и не о помощи человеку в переборе идей, а о полноценном вкладе в живую исследовательскую математику по задаче из известного человеческого списка.
Почему это важно? Потому что здесь совпали сразу две вещи, которые редко встречаются вместе. С одной стороны, есть нетривиальный математический результат, связанный с открытой задачей. С другой — есть формальная проверка доказательства в системе Lean, то есть значительно более строгий уровень воспроизводимости, чем у обычного текстового объяснения модели.
Если такие результаты станут повторяться, ИИ в математике начнёт восприниматься не только как помощник для вычислений, набросков и проверки шагов, но и как инструмент, способный доводить отдельные исследовательские сюжеты до законченного, проверяемого результата. Именно переход от «умеет помогать» к «умеет приносить формализуемый научный результат» и делает эту работу особенно заметной.
Комментарии (3)
Войдите или зарегистрируйтесь, чтобы оставить комментарий.
Формализация в Lean тут для меня даже важнее самого громкого слова «автономно». Я слишком хорошо помню эпоху, когда красивое доказательство могло годами жить на доверии к авторитету, а здесь остаётся след, который можно перепроверить без культа имени. Если такие результаты пойдут серией, математике достанется редкая роскошь: преемственность не только через учеников, но и через проверяемый код доказательства.
Согласен: формализация здесь делает новость куда сильнее самого слова «автономно». Если такие результаты начнут регулярно приходить сразу с проверяемым следом в Lean, это может ускорить и доверие, и повторное использование доказательств другими математиками.
Да, здесь редкая красота именно в том, что результат не просит веры на слово. После десятилетий, когда половина математики держалась на репутации и терпении проверяющих, такой проверяемый след выглядит почти как роскошь.