Петер Шолце иска да възстанови голяма част от съвременната математика, като започне от един от нейните крайъгълни камъни. Сега той е получил потвърждение за доказателство в основата на своето търсене от малко вероятен източник: компютър.
Въпреки че повечето математици се съмняват, че машините ще заменят творческите аспекти на тяхната професия в скоро време, някои признават, че технологията ще играе все по-важна роля в техните изследвания — и този конкретен подвиг може да бъде повратна точка към приемането ѝ.
Шолце, теоретик на числата, изложи амбициозния план — който той създаде съвместно със своя сътрудник Дъстин Клаузен от университета в Копенхаген — в поредица от лекции през 2019 г. в университета в Бон, Германия, където се намира . Двамата изследователи го нарекоха „кондензирана математика“ и казват, че обещава да донесе нови прозрения и връзки между области, вариращи от геометрия до теория на числата.
Други изследователи обръщат внимание: Шолце се смята за една от най-ярките звезди на математиката и има опит във въвеждането на революционни концепции. Емили Рийл, математик от университета Джон Хопкинс в Балтимор, Мериленд, казва, че ако визията на Шолце и Клаузен бъде реализирана, начинът, по който математиката се преподава на студентите след 50 години, може да бъде много по-различен от този днес. „Има много области на математиката, които според мен ще бъдат повлияни от неговите идеи в бъдеще“, казва тя.
Досега голяма част от тази визия се основаваше на техническо доказателство, толкова ангажирано, че дори Шолце и Клаузен не можеха да бъдат сигурни, че е правилно. Но по-рано този месец Шолце обяви, че проект за проверка на сърцевината на доказателството с помощта на специализиран компютърен софтуер е бил успешен.
Компютърна помощ
Математиците отдавна използват компютри, за да правят числени изчисления или да манипулират сложни формули. В някои случаи те са доказали големи резултати, като карат компютрите да извършват огромни количества повтаряща се работа - най-известният е доказателство през 70-те години на миналия век, че всяка карта може да бъде оцветена само с четири различни цвята и без да се запълват две съседни държави с един и същи цвят.
Вундеркинд на теорията на числата сред носителите на най-желаната награда по математика
Но системите, известни като асистенти за доказване, отиват по-дълбоко. Потребителят въвежда изрази в системата, за да я научи на дефиницията на математическа концепция - обект - въз основа на по-прости обекти, за които машината вече знае. Твърдението може също така просто да се отнася до известни обекти и асистентът за доказателство ще отговори дали фактът е „очевидно“ верен или неверен въз основа на текущите му познания. Ако отговорът не е очевиден, потребителят трябва да въведе повече подробности. По този начин асистентите за доказване принуждават потребителя да изложи логиката на своите аргументи по строг начин и попълват по-прости стъпки, които човешките математици съзнателно или несъзнателно са пропуснали.
След като изследователите са свършили упоритата работа по превеждането на набор от математически концепции в помощник за доказване, програмата генерира библиотека от компютърен код, който може да бъде надграден от други изследователи и използван за дефиниране на математически обекти от по-високо ниво. По този начин асистентите за доказване могат да помогнат за проверка на математически доказателства, които иначе биха отнели много време и биха били трудни, може би дори практически невъзможни, за проверка от човек.
Асистентите за доказателство отдавна имат своите фенове, но това е първият път, когато те имат важна роля в авангарда на дадена област, казва Кевин Бъзард, математик от Imperial College London, който участва в сътрудничество, което проверява Резултатът на Шолце и Клаузен. „Големият оставащ въпрос беше: могат ли да се справят със сложна математика?“ казва Бъзард. "Показахме, че могат."
И всичко се случи много по-бързо, отколкото някой си е представял. Шолце изложи предизвикателството си към експертите по доказване през декември 2020 г. и то беше прието от група доброволци, ръководени от Йохан Комелин, математик от университета на Фрайбург в Германия. На 5 юни - по-малко от шест месеца по-късно - Шолце публикува в блога на Buzzard, че основната част от експеримента е успешна. „Смятам, че е абсолютно безумно, че интерактивните асистенти за доказване сега са на ниво, че в рамките на много разумен период от време, те могат официално да проверят трудни оригинални изследвания“, пише Шолце.
Математиката с изкуствен интелект създава трудни нови проблеми за решаване от хората
Решаващият момент на кондензираната математика, според Шолце и Клаузен, е да предефинира концепцията за топология, един от крайъгълните камъни на съвременната математика. Много от обектите, които математиците изучават, имат топология - тип структура, която определя кои от частите на обекта са близо една до друга и кои не. Топологията дава представа за форма, но такава, която е по-гъвкава от тези на познатата геометрия на училищно ниво: в топологията всяка трансформация, която не разкъсва обект, е допустима. Например, всеки триъгълник е топологично еквивалентен на всеки друг триъгълник - или дори на кръг - но не и на права линия.
Топологията играе решаваща роля не само в геометрията, но и във функционалния анализ, изследването на функциите. Функциите обикновено „живеят“ в пространства с безкраен брой измерения (като вълнови функции, които са основополагащи за квантовата механика). Също така е важно за числови системи, наречени p-адични числа, които имат екзотична, „фрактална“ топология.
Голямо обединение
Около 2018 г. Шолце и Клаузен започнаха да осъзнават, че конвенционалният подход към концепцията за топология води до несъвместимост между тези три математически вселени — геометрия, функционален анализ и p-адични числа — но че алтернативните основи могат да преодолеят тези пропуски. Много резултати във всяка от тези области изглежда имат аналози в другите, въпреки че очевидно се занимават с напълно различни концепции. Но след като топологията е дефинирана по „правилния“ начин, аналогиите между теориите се разкриват като случаи на една и съща „кондензирана математика“, предложиха двамата изследователи. „Това е някакво велико обединение“ на трите полета, казва Клаузен.
Шолце и Клаузен казват, че вече са намерили по-прости, „кондензирани“ доказателства за редица дълбоки геометрични факти и че сега могат да доказват теореми, които преди са били неизвестни. Те все още не са ги направили публично достояние.
Имаше обаче една уловка: за да покажат, че геометрията се вписва в тази картина, Шолце и Клаузен трябваше да докажат една изключително техническа теорема за множеството от обикновени реални числа, което има топологията на права линия. „Това е като основополагащата теорема, която позволява на реалните числа да влязат в тази нова рамка“, обяснява Комелин.
Клаузен си спомня как Шолце работи безмилостно върху доказателството, докато не бъде завършено „чрез силата на волята“, произвеждайки много оригинални идеи в процеса. „Това беше най-невероятният математически подвиг, на който някога съм бил свидетел“, спомня си Клаузен. Но аргументът беше толкова сложен, че самият Шолце се притесняваше, че може да има някаква фина празнина, която да обезсили цялото начинание. „Изглеждаше убедително, но просто беше твърде ново“, казва Клаузен.
За помощ при проверката на тази работа Шолце се обърна към Бъзард, колега теоретик на числата, който е експерт по Lean, софтуерен пакет за асистент за доказване. Lean първоначално е създаден от компютърен учен в Microsoft Research в Редмънд, Вашингтон, с цел стриктна проверка на компютърния код за грешки.
Buzzard изпълняваше многогодишна програма за кодиране на цялата учебна програма по математика в Imperial в Lean. Той също така експериментира с въвеждането на по-напреднала математика в системата, включително концепцията за перфектоидните пространства, което помогна на Шолце да спечели медал на Фийлдс през 2018 г.
Комелин, който също е теоретик на числата, пое инициативата да потвърди доказателството на Шолце и Клаузен. Commelin и Scholze решиха да нарекат своя Lean проект Liquid Tensor Experiment, в знак на почит към прогресив-рок групата Liquid Tension Experiment, на която и двамата математици са фенове.
Последва трескаво онлайн сътрудничество. Дузина или повече математици с опит в Lean се присъединиха и изследователите получиха помощ от компютърни учени по пътя. До началото на юни екипът напълно преведе сърцето на доказателството на Шолце - частта, която го тревожеше най-много - в Lean. И всичко беше проверено - софтуерът успя да провери тази част от доказателството.
По-добро разбиране
Лейн версията на доказателството на Шолце се състои от десетки хиляди редове код, 100 пъти по-дълги от оригиналната версия, казва Комелин. „Ако просто погледнете Lean кода, ще ви е много трудно да разберете доказателството, особено по начина, по който е сега.“ Но изследователите казват, че усилията да накарат доказателството да работи в компютъра им е помогнало да го разберат по-добре.
ВРЪЗКА AI Коперник „открива“, че Земята обикаля около Слънцето
Рийл е сред математиците, които са експериментирали с асистенти за доказателство, и дори им преподава в някои от студентските си курсове. Тя казва, че въпреки че не ги използва систематично в изследванията си, те са започнали да променят самия начин, по който мисли за практиките на конструиране на математически концепции и формулиране и доказване на теореми за тях. „Преди мислех за доказване и конструиране като за две различни неща, а сега ги смятам за едно и също.“
Много изследователи казват, че математиците едва ли скоро ще бъдат заменени от машини. Помощниците за доказване не могат да четат учебник по математика, те се нуждаят от непрекъснат принос от хора и не могат да решат дали дадено математическо твърдение е интересно или задълбочено – само дали е правилно, казва Бъзард. Все пак компютрите скоро може да са в състояние да посочат последствията от известните факти, които математиците не са забелязали, добавя той.
Шолце казва, че е бил изненадан от това колко далеч могат да стигнат асистентите за доказване, но не е сигурен дали те ще продължат да играят основна роля в неговите изследвания. „Засега не виждам как биха ми помогнали в творческата ми работа като математик.“
