Нови ли са деветте доказателства на DeepMind?

Математическото доказателство може да изглежда безупречно и все пак да крие пропуск, който никой не забелязва с години. ИИ агентът AlphaProof Nexus на Google DeepMind е доказал девет задачи, поставени от Пол Ердьош, а софтуер е проверил всяка стъпка. Работата се появява първо като предпечатна публикация през май (arXiv), а на 8 октомври е публикувана в Science след рецензиране (Science). Софтуерът може да потвърди логиката, но дали тя носи нещо ново трябва да преценят математици.

Арбитър, който не се впечатлява от стила

Чатботовете умеят да пишат математика, която звучи убедително. Увереният тон може да прикрие пропусната стъпка, а тя се открива само при внимателно четене. AlphaProof Nexus избягва този проблем, като работи с Lean — език за програмиране, в който определенията, твърденията и доказателствата се формулират достатъчно точно, за да може компютър да ги провери.

Lean е като арбитър, който проверява всеки ред от завършеното доказателство по фиксирани правила. Стилът няма значение. Ако една стъпка не следва от предишните, доказателството не издържа проверката, колкото и елегантно да изглежда останалото.

Екипът описва агента като система, която търси доказателства, написани на Lean. Изследователите са му дали достъп и до AlphaProof — по-ранна система на DeepMind, създадена специално за доказателства. В изпитанията им по-опростена конфигурация дала същите резултати: езиков модел, свързан с Lean, но без AlphaProof, също намерил доказателства за всичките девет задачи на Ердьош (The Decoder). За тези задачи специализираната система се оказала излишна.

Статията съобщава за приети доказателства на деветте твърдения на Ердьош и на 44 хипотези от Online Encyclopedia of Integer Sequences — обширен каталог на числови закономерности (Science). Сред резултатите на Ердьош е въпрос от две части за целите числа, който той и Андраш Шаркьози поставят през 1970 г. Той остава нерешен повече от половин век (ABC).

Какво не може да прецени арбитърът

Гаранцията на Lean има ясна граница: системата потвърждава, че доказателството установява точно твърдението, формулирано в кода. Три въпроса остават извън обхвата ѝ: дали кодът предава смисъла, вложен от Ердьош; дали някой не е отговорил на въпроса по-рано; и дали отговорът добавя нещо към математиката.

Задачата от 1970 г. показва защо последните два въпроса имат значение. Втората ѝ част предполага първата, така че едно доказателство решава и двете. След като доказателствата на агента стават публични, се оказва, че и двете части могат да се решат с малка промяна в конструкция от оригиналната статия от 1970 г. (arXiv). Доказателствата на агента са коректни. Просто задачата се оказва била по-близо до решение, отколкото подсказва обозначението ѝ като „нерешена“.

Това се установява с помощта на хора, които познават областта. Гергей Берци, математик от Aarhus University в Дания и един от авторите, помага да се подберат подходящи задачи и да се проверят решенията (Aarhus University). Той помага и да се подготвят варианти на доказателствата, които човек може да следи. Lean потвърждава всеки ред, а Берци и колегите му преценяват какво означават редовете като цяло.

Това разделение на труда отличава изследването от постижение от миналия месец. Тогава Claude на Anthropic превръща вече известно доказателство на последната теорема на Ферма във формална версия на Lean (To Brief). При превръщането на известно доказателство в код няма съмнение за новостта. Търсенето на решение сред твърдения, смятани за нерешени, поставя този въпрос на преден план.

Екипът е публикувал файловете с доказателствата, така че други могат да ги проверят със същия арбитър (GitHub). Изследването показва конкретен напредък: ИИ агент е създал доказателства, проверими от машина, за някои твърдения, които математиците са смятали за нерешени. Гаранцията се отнася до твърденията така, както са формулирани на Lean. Какво ново внася всяко доказателство в математиката, преценяват математиците, които го четат.