AI в математиката: десет решени задачи и нула рецензии

5.08

време за четене: 3 мин.

На 1 август 2026 г. OpenAI публикува 249 страници с решения на десет отворени задачи в математиката и теоретичната информатика. Заедно с тях излезе и нещо по-необичайно: над половин милион реда код в Lean 4, който позволява всяко доказателство да бъде проверено машинно. Компилаторът не приема преразказ.

Робот подава дебела купчина листове на математик пред черна дъска, а математикът държи празен печат и се оглежда за кой да го подпише.

Какво съдържа публикацията

Хранилището "openai/ten-proofs" се появява на 1 август 2026 г. под лиценз Apache 2.0. В него има десет файла на Lean 4, общо 548 205 реда, компилирани с версия 4.32.0 на езика. Нито един не съдържа "sorry" - маркерът, с който Lean отбелязва пропусната стъпка. Използваните аксиоми са само трите стандартни за езика.

Сред задачите са първата явна конструкция на несофична група, което отговаря на въпрос, поставен от Михаил Громов през 1999 г., опровержение на хипотезата на Кон за твърдост, хипотезата на Ерхарт за обема и три задачи на Ердьош под номера 183, 146 и 180. Останалите са в областта на сферичните опаковки, кодирането, аритметичната сложност и квантовото паралелно повторение.

Разходът за токени е около 2 000 щатски долара по тарифите на Sol API. Forbes добавя уточнение, което променя мащаба на числото: това е цената на публикуването, не на откриването. Сумата покрива успешните пускания, не всички опити.

Защо сертификатът в Lean е новото

През октомври 2025 г. OpenAI вече обяви, че GPT-5 е решил десет нерешени задачи на Ердьош. Оказа се, че моделът е намерил вече публикувани решения, които каталогът просто не е отразявал. Томас Блум, който поддържа списъка, определи съобщението като „драматично изопачаване" и уточни, че моделът е намерил източници, които той лично не е познавал. Публикацията беше изтрита, а Демис Хасабис я нарече смущаваща.

Сертификатът в Lean премахва точно този провал. Компилаторът дава двоичен отговор: доказателството или следва от твърдението, или не следва. Убеждаване няма, авторитет не помага.

Той обаче гарантира по-малко, отколкото изглежда на пръв поглед. Lean проверява, че доказателството следва от формалното твърдение. Не проверява, че формалното твърдение е същата задача, която математиците смятат за отворена, нито че резултатът е нов.

Какво липсва

Нито един от десетте резултата не е минал рецензия от колеги. Във файла с метаданни на формализацията статусът на прегледа е записан като „agent-reviewed", тоест прегледано от агент.

Ърни Дейвис поставя и въпроса за подбора: „Ако са подбрали 50 хипотези, за които са смятали, че Astra ще се справи, и тя е успяла с 10, това пак е забележително, но значително по-малко."

Гари Маркъс насочва към друга празнина: „пусна статия от 249 страници с нови математически резултати, но нито една страница не е за това как работи моделът, как са проверени доказателствата и каква роля, ако изобщо, са изиграли хората."

Отделно моделът не е публично достъпен. Резултатите могат да бъдат проверени, но не и възпроизведени от независим екип.

Какво променя това за AI в математиката

Още през юни 2026 г., два месеца преди този анонс, над хиляда математици подписаха Лайденската декларация. Питър Шолце формулира позицията ѝ така: „целта на математическото изследване е човешкото разбиране на математиката, затова математиката може да процъфтява само в общност от човешки изследователи."

Двете твърдения не са в противоречие. Спорът за AI в математиката не е дали машината смята вярно. Машината произведе нещо проверимо ново; общността настоява, че проверимостта не е цялата стойност. Между тях остава работата, която не се автоматизира: изборът кой въпрос заслужава внимание, преценката дали резултатът е важен и рецензията.

За хората, които се готвят за професия, тук има по-полезен извод от спора за замяната. Когато резултатът идва със сертификат, доверието спира да зависи от името на автора. Умението, което поскъпва, не е да се знае отговорът, а да се формулира въпросът и да се провери твърдението.

Заключение

Astra доказа десет теореми и нито едно от обичайните твърдения около такъв анонс. Разликата между „компилира" и „прието от науката" е точно мястото, където работата на хората остава.

Помагаме на български организации и екипи да четат съобщенията за AI пробиви по същество, а не по заглавие - включително когато числата са реални, но означават друго. Услугите ни покриват одит, оценка на готовност, обучение на екипи и имплементация на специализирани AI автоматизации за всяка организация. Препоръчваме консултация при оценка дали конкретна AI способност е приложима към Вашите задачи. [Свържете се с нас за консултация: academy@razvivai.se]