Новости науки (самые разные)

[Н. Светлов]

An internal OpenAI system

Это стало известно из пресс-релиза компании. Но есть мнение, что решение найдено всё-таки не ею, а живыми людьми. Запасаемся поп-корном и наблюдаем за очередой, осовремененной, итерацией шоу имени Ньютона-Лейбница

[Весельчак Ы]

Я пытался читать это доказательство, но я далеко не дифурщик и быстро увяз. Однако, насколько я вижу, предлагаемый пример очень сложный, он требует согласования многих фрагментов, а в таких конструкциях LLMы могут и превосходить людей.

[Н. Светлов]

а в таких конструкциях LLMы могут и превосходить людей

Это не отрицается. Предполагаемый автор доказательства признаёт, что использовал LLMы в своей работе. Но утверждает, что доказательство получил всё-таки он, а нейросеть от OpenAI воспроизвела его (в ином варианте) лишь потому, что обучалась в том числе на материалах обсуждений, в которых принимал участие автор доказательства, изложив там ключевые идеи. В OpenAI согласились, что этот материал, возможно, был использован при обучении, наряду с прочими открытыми данными, но всё же настаивают на том, что задачу решила их нейросеть.

Во всяком случае, утверждение о том, что нейросети научились самостоятельно решать математические проблемы высшей категории сложности, немножко подвисло.

► Показать

Да это и невозможно в принципе, ибо известно, что не существует такого алгоритма, который мог бы отыскать доказательство любой наперёд заданной теоремы теории чисел (а значит, и теорий, имеющих теорию чисел в своей основе). Отсюда естественный, хотя и не строгий, вывод о том, что кое-что из доказанного людьми не доказуемо алгоритмически (аргумент Пенроуза) — в том числе не под силу никакой нейросети, существующей или будущей.

[Весельчак Ы]

Н. Светлов, вот свежий трэд "Relevance of the work of Alpöge and Buckmaster to Navier-Stokes?" с MathOverflow.
В частности, там

Building on work of Diego Córdoba and Luis Martínez-Zoroa, Tristan Buckmaster and Levent Alpöge have made major progress toward a negative solution to the Navier–Stokes Millennium Prize Problem.

и приводится ссылка на открытое письмо Buckmasterа.

[Н. Светлов]

и приводится ссылка на открытое письмо Buckmasterа

Отсюда становится ясно, что вклад нейросети, по меньшей мере, весьма существенен. Доказательство-то она нашла, хотя и не похоже, чтобы она смогла бы найти его без взаимодействия с людьми, направлявшими её в нужное русло.

Остальные тёрки мне не особенно интересны

[Весельчак Ы]

не существует такого алгоритма, который мог бы отыскать доказательство любой наперёд заданной теоремы теории чисел (а значит, и теорий, имеющих теорию чисел в своей основе)

Насколько я знаю и понимаю, как мне кажется, и, наверное, так и есть, это не так: Прежде всего, существует простой алгоритм, который, рано или поздно, докажет любую теорему -- для этого достаточно перебирать все возможные доказательства, которых, по сути, счётное число. Алгоритма же, наверное, не существует для определения того, является ли данное утверждение теоремой (то есть, доказуемо), или нет. Но для расширения теории чисел, это, вообще говоря, может быть неверным. Возможно, здесь ситуация аналогична теореме Гёделя о неполноте арифметики S и ее расширений. Ибо по лемме Линденбаума, непротиворечивая теория первого порядка имеет непротиворечивое и полное расширение. Но дело в том, что это расширение может не быть рекурсивно аксиоматизированной теорией, даже если исходная теория такова. Теорема же Гёделя о неполноте относится к рекурсивно аксиоматизированным теориям. И, наконец, непротиворечивость аксиоматической теории множеств Цермело-Френкеля (Con ZFC) не только неизвестна, а вообще недоказуема.

[Н. Светлов]

Прежде всего, существует простой алгоритм, который, рано или поздно, докажет любую теорему -- для этого достаточно перебирать все возможные доказательства, которых, по сути, счётное число.

Перепроверил. Да, это так. Алгоритм существует. Но лишь в том случае, если каким-то образом заранее подготовлен список доказуемых формул (теорем). Если же такого списка нет, то мы оказываемся в условиях теоремы Тарского, и алгоритм увязает в бесконечных рекурсиях, не устранимых ни при одной стратегии обхода дерева. По крайней мере, так обстоит дело с арифметикой Пеано и теми её расширениями, которые выразимы её собственными формулами.

За довод спасибо: он стал поводом лишний раз покопаться во всех этих нюансах — в частности, научиться различать термины «computably enumerable» и «computably provable».

Моя ошибка в том, что я написал «доказательство любой наперёд заданной теоремы». Правильно было бы «доказательство для любой наперёд заданной формулы, если она доказуема».