ИИ AxiomProver доказал математическую гипотезу, над которой исследователи работали пять лет
NewsMakerПока одни чатились с нейросетью, другая система взяла и доказала настоящую теорему.
Пять лет назад математики Давэй Чэнь и Квентен Жандрон работали над сложной задачей из алгебраической геометрии, связанной с дифференциалами, то есть инструментами анализа, которые помогают измерять «расстояния» вдоль искривленных поверхностей. В какой-то момент их рассуждение уперлось в неожиданную проблему: ключевой шаг опирался на необычную формулу из теории чисел, но исследователи не смогли ни доказать ее, ни аккуратно обосновать. В итоге результат пришлось оформить как гипотезу, а не как теорему.
Недавно Чэнь попытался вернуться к этой задаче с помощью ChatGPT, часами подбирая запросы в надежде получить рабочее доказательство, но заметного прогресса не было. Перелом случился на конференции по математике в Вашингтоне: на приеме Чэнь встретил Кена Оно, известного математика, который недавно ушел из Университета Вирджинии и присоединился к стартапу Axiom . Компания разрабатывает ИИ-инструменты для доказательства теорем, а одним из ее сооснователей стала Карина Хонг, бывшая ученица Оно.
Чэнь рассказал Оно о своей нерешенной проблеме, и уже на следующее утро получил готовое доказательство, которое сгенерировала система AxiomProver. По словам Чэня, после этого «все естественно встало на свои места». Вместе с командой Axiom он оформил материал в статью, и теперь она опубликована на arXiv .
Как описывает Axiom, их инструмент нашел связь между задачей Чэня и Жандрона и числовым явлением, которое впервые изучали еще в XIX веке. Затем система построила доказательство и, что особенно важно для математики, самостоятельно проверила его корректность. Оно утверждает, что ИИ заметил то, что упустили люди.
Пять лет назад математики Давэй Чэнь и Квентен Жандрон работали над сложной задачей из алгебраической геометрии, связанной с дифференциалами, то есть инструментами анализа, которые помогают измерять «расстояния» вдоль искривленных поверхностей. В какой-то момент их рассуждение уперлось в неожиданную проблему: ключевой шаг опирался на необычную формулу из теории чисел, но исследователи не смогли ни доказать ее, ни аккуратно обосновать. В итоге результат пришлось оформить как гипотезу, а не как теорему.
Недавно Чэнь попытался вернуться к этой задаче с помощью ChatGPT, часами подбирая запросы в надежде получить рабочее доказательство, но заметного прогресса не было. Перелом случился на конференции по математике в Вашингтоне: на приеме Чэнь встретил Кена Оно, известного математика, который недавно ушел из Университета Вирджинии и присоединился к стартапу Axiom . Компания разрабатывает ИИ-инструменты для доказательства теорем, а одним из ее сооснователей стала Карина Хонг, бывшая ученица Оно.
Чэнь рассказал Оно о своей нерешенной проблеме, и уже на следующее утро получил готовое доказательство, которое сгенерировала система AxiomProver. По словам Чэня, после этого «все естественно встало на свои места». Вместе с командой Axiom он оформил материал в статью, и теперь она опубликована на arXiv .
Как описывает Axiom, их инструмент нашел связь между задачей Чэня и Жандрона и числовым явлением, которое впервые изучали еще в XIX веке. Затем система построила доказательство и, что особенно важно для математики, самостоятельно проверила его корректность. Оно утверждает, что ИИ заметил то, что упустили люди.