Последната теорема на Ферма е озадачавала математиците в продължение на векове, докато най-накрая била доказана през 1993 г. Сега изследователите искат да създадат версия на доказателството, което може да бъде официално проверено от компютър за логически грешки.
Математици се надяват да разработят компютъризирано доказателство на последната теорема на Ферма в амбициозен, многогодишен проект, който има за цел да демонстрира потенциала на компютърно подпомогнатите математически доказателства.
ОЩЕ: Десетичната точка се появила 150 години по-рано от известното
Теоремата на Пиер дьо Ферма, която той за първи път предлага около 1637 г., гласи, че няма цели положителни числа, a, b и c, които да отговарят на уравнението an + bn = cn за всяко цяло число n, по-голямо от 2. Ферма надрасква твърдението в полето на книгата „Аритметика“ на Диофант. В бележката Ферма твърди, че доказателството е прекалено дълго, за да се смести в границите на полето.
Едва през 1993 г. Андрю Уайлс, тогава в Принстънския университет, „подпалва“ математическия свят, като обявява, че разполага с доказателство. Обхващайки повече от 100 страници, доказателството съдържа толкова напреднала математика, че на колегите му са необходими повече от две години, за да се уверят, че не съдържа никакви грешки.
Много математици се надяват, че тази работа по проверка и евентуално писане на доказателства може да бъде ускорена чрез превода им на компютърно четим език. Този процес на формализация би позволил на компютрите незабавно да забележат логически грешки и потенциално да използват теоремите като градивни елементи за други доказателства.
Но формализирането на съвременните доказателства само по себе си може да бъде трудно и отнемащо време, тъй като голяма част от съвременната математика, на която разчитат, тепърва ще бъде направена машинно четима. Поради тази причина формализирането на последната теорема на Ферма дълго време се смяташе за далеч недостижимо.
Сега Кевин Бъзард и колегите му от Имперския колеж в Лондон обявиха планове да поемат предизвикателството, опитвайки се да формализират последната теорема на Ферма в език за програмиране, наречен Lean, пише New Scientist.
„Няма смисъл от последната теорема на Ферма, тя е напълно безсмислена. Тя няма никакви приложения – нито теоретични, нито практически – в реалния свят“, казва Бъзард. „Но това наистина е труден въпрос, станал печално известен, защото в продължение на векове хората са генерирали купища брилянтни нови идеи в опит да го разрешат.“
Той се надява, че формализирането на много от тези идеи, които сега включват рутинни математически инструменти в теорията на числата, като модулни форми и представяния на Галоа, ще помогне на други изследователи, чиято работа в момента е твърде далеч извън обхвата на компютърните асистенти.
„Това е вид проект, който може да има доста широкообхватни и неочаквани ползи и последствия“, казва Крис Уилямс от университета в Нотингам, Великобритания.
Самото доказателство ще следва донякъде това на Уайлс, с леки модификации. Публично достъпен план ще бъде достъпен онлайн, след като проектът стартира през април, така че всеки от бързо развиващата се общност на Lean да може да допринесе за формализиране на части от доказателството.
ОЩЕ: Гениална или заимствана е Питагоровата теорема?
„Преди десет години това щеше да отнеме безкрайно много време“, казва Бъзард. Въпреки това той ще се съсредоточи върху проекта на пълен работен ден от октомври, като ще отложи преподавателските си задължения за пет години в опит да го завърши.
„Мисля, че е малко вероятно той да успее да формализира цялото доказателство през следващите пет години, това би било зашеметяващо постижение – коментира Уилямс. – Но тъй като много от инструментите, които влизат в него, са толкова повсеместни сега в теорията на числата и аритметичната геометрия, очаквам някакъв значителен напредък към това да бъде много полезно в бъдеще.“
