В чем заключается открытие?
Математическое сообщество было потрясено новостью о том, что агент искусственного интеллекта смог подтвердить правильность решения сложнейшей задачи об упаковке сфер в многомерных пространствах. Это доказательство, касающееся случаев в 8-мерном и 24-мерном пространствах, принесло украинскому математику Марине Вязовской престижную медаль Филдса в 2022 году. До ее прорыва эта задача была полностью решена только для одного, двух и трех измерений, тогда как все остальные варианты оставались открытыми в течение десятилетий, пишет Live Science.
Смотрите также Google запускает Gemini в Chrome для новых стран и добавляет украинский язык
Это событие знаменует собой начало тихой революции. На протяжении веков ученые использовали вспомогательные средства – от абака и логарифмических линеек до калькуляторов и компьютеров. Однако раньше эти инструменты лишь ускоряли вычисления, не заменяя человека в процессе рассуждения. Теперь ситуация изменилась: современные системы помогают выстраивать логические цепочки и выполнять рутинные операции, лежащие в основе интеллектуального труда.
Ключевую роль в процессе верификации сыграл ИИ-агент Gauss, разработанный стартапом Math. Он работал в тандеме с формальным языком программирования Lean, который специально создан для проверки математических аргументов. В отличие от обычных научных текстов, Lean требует абсолютной четкости в каждом определении и выводе, исключая любые скрытые предположения или интуитивные прыжки. Если программа принимает аргумент, это гарантирует его полную логическую корректность.
Процесс верификации выглядел как слаженная работа команды: люди создали общую структуру и концептуальный каркас доказательства, а искусственный интеллект заполнял пробелы. Эффективность машины оказалась удивительной.
- Работу над восьмимерным случаем, которую исследователи планировали выполнять в течение нескольких месяцев, алгоритм завершил всего за несколько дней.
- Более сложная задача для 24-мерного пространства также была успешно решена вскоре после этого.
Известный математик Теренс Тао, который также является лауреатом медали Филдса, отмечает, что главная ценность таких технологий заключается в освобождении ученых от рутинной работы. Искусственный интеллект берет на себя тысячи мелких, хотя и логически понятных случаев, которые отнимают слишком много времени при ручной обработке. Это позволяет исследователям сосредоточиться на стратегии и творческом поиске идей, оставляя формальную проверку машинам.
В то же время эксперт Кевин Баззард из Имперского колледжа Лондона обращает внимание на важную деталь: несмотря на то, что большие языковые модели могут звучать убедительно, они не гарантируют точности. Именно поэтому использование специализированных языков верификации, таких как Lean, является критически важным. Главным вызовом остается то, что большинство современной математики еще не переведено на язык, понятный таким системам.
Несмотря на стремительное развитие технологий, ученые убеждены, что математики не исчезнут как профессия. Наоборот, возникает острая потребность в специалистах, способных ставить правильные вопросы, создавать новые концепции и распознавать настоящую глубину идей. Ученые будущего будут все больше напоминать разработчиков сложных инструментов, сочетающих человеческую интуицию с машинной настойчивостью для достижения абсолютной уверенности в результатах.