Модель искусственного интеллекта представила доказательство существования чистой теории Янга–Миллса, и эксперты подтвердили его формальную проверку. Однако это лишь первая часть одной из задач тысячелетия: вопрос о массовой щели остается нерешенным, а сами специалисты признают, что пока не полностью понимают доказательство.
Эксперты, привлеченные для проверки математических решений, созданных ИИ, заявили, что результат соответствует постановкам задач, принятым в физике и математике. К его оценке присоединился профессор Дэвид Гросс, физик-теоретик и лауреат Нобелевской премии. Гросс и его коллеги опубликовали пояснения и подтверждение формальной проверки доказательства на языке программирования Lean, предназначенном для верификации математических работ.
«Мы сообщаем об обновлении статуса работы нашего комитета по сопровождению результата, полученного большой языковой моделью», — заявили эксперты во главе с профессором.
Математик Скотт Армстронг из Нью-Йоркского университета приветствовал публикацию кода:
«Я рад, что „пастухи“ наконец публикуют доказательство на Lean, так что мы можем увидеть, в чем состоит результат. Надеюсь, что в будущем разработчики ИИ будут широко делиться своими результатами с сообществом. Такую проверку можно провести более эффективно и быстро в открытом режиме».
Проблема Янга–Миллса входит в число пяти нерешенных «Проблем тысячелетия» из семи задач, сформулированных Математическим институтом Клэя в 2000 году. За решение каждой предусмотрена премия в миллион долларов. Но для науки особое значение имело бы не только денежное вознаграждение: решение могло бы устранить математическую нестрогость в описании физики элементарных частиц.
Стандартная модель — одна из самых тщательно проверенных научных теорий. Она точно предсказывает результаты столкновений субатомных частиц на установках вроде Большого адронного коллайдера. Однако до сих пор не удалось свести ее положения к простым аксиомам и тем самым доказать ее математическую состоятельность.
Задача о теории Янга–Миллса состоит из двух частей. Первая требует доказать, что теория, лежащая в основе Стандартной модели, математически существует и может быть построена корректными шагами. Вторая — более сложная и количественная — предполагает показать, что из уравнений Янга–Миллса следует наличие массовой щели. По данным компании, модель решила только первую часть.
Авторы оценки отмечают, что опубликованных пояснений пока недостаточно для глубокого понимания доказательства. Гросс и его коллеги, хотя все пятеро занимались теорией Янга–Миллса, также говорят, что пока не вполне разобрались в нем.
«Мы воспользовались Astra от OpenAI для осмысления представленного кода на Lean. Мы пока не утверждаем, что полностью понимаем доказательство», — пояснили они в своей оценке.
Публикация доказательства и кода Lean открывает возможность для дальнейшего изучения результата и его проверки математическим сообществом.