OpenAI сообщает, что их ИИ нашёл доказательства для трёх научных…

OpenAI сообщает, что их ИИ нашёл доказательства для трёх научных задач, которые не поддавались годами. Гипотеза Согге о локальном сглаживании стоит с 1991 года, доказательство получено 18 октября, формализовано в Lean на следующий день. Опровергнута гипотеза экспоненциального времени, на которой основаны сотни работ по информатике. Предложены доказательства, связанные с задачей тысячелетия Янга-Миллса, их разбирает группа во главе с Дэвидом Гроссом.

Для бизнеса это пока не инструмент, а сигнал: модели умеют строить формальные доказательства, проверяемые в Lean, а не просто выдавать правдоподобный текст. Экспертиза ещё идёт, часть материалов не опубликована, прикладной пользы из опровержения ETH пока нет.

Доказательство в Lean и опровержение ETH звучат громко, но пока это непроверенные рукописи, а не готовое знание. Для своей работы беру на заметку саму идею: формальная верификация выводов ИИ, а не вера на слово, пригодится и в куда более приземлённых задачах вроде проверки расчётов в ботах.

Илья

Источник: @ai_machinelearning_big_data, https://t.me/ai_machinelearning_big_data/11215