Gündem

Matematikçiler ‘büyük birleşme’ teorisinde bilgisayar destekli kanıtı memnuniyetle karşılıyor

0

Fas'ın merkezi şehri Khouribga'daki bilgi teknolojisi eğitim merkezindeki bilgisayar laboratuvarı

Bilgisayarları kullanarak karmaşık bir matematiksel ispatı doğrulama çabaları başarılı olmuştur.Kredi: Getty aracılığıyla Fadel Senna/AFP

Peter Scholze, temel taşlarından birinden başlayarak modern matematiğin çoğunu yeniden inşa etmek istiyor. Şimdi, arayışının kalbinde yer alan bir kanıt için, beklenmedik bir kaynaktan onay aldı: bir bilgisayar.

Çoğu matematikçi, makinelerin yakın zamanda mesleklerinin yaratıcı yönlerinin yerini alacağından şüphe duysa da, bazıları teknolojinin araştırmalarında giderek daha önemli bir rol oynayacağını kabul ediyor – ve bu özel başarı, kabul edilmesi için bir dönüm noktası olabilir.

Bir sayı teorisyeni olan Scholze, Kopenhag Üniversitesi’nden işbirlikçisi Dustin Clausen ile birlikte oluşturduğu iddialı planı, 2019 yılında bulunduğu Almanya’nın Bonn Üniversitesi’nde bir dizi derste ortaya koydu. İki araştırmacı buna ‘yoğunlaştırılmış matematik’ adını verdi ve geometriden sayı teorisine kadar alanlar arasında yeni anlayışlar ve bağlantılar getirmeyi vaat ettiğini söylüyorlar.

Diğer araştırmacılar dikkat ediyor: Scholze, matematiğin en parlak yıldızlarından biri olarak kabul ediliyor ve devrim niteliğinde kavramları tanıtma konusunda bir geçmişe sahip. Maryland, Baltimore’daki Johns Hopkins Üniversitesi’nde matematikçi olan Emily Riehl, Scholze ve Clausen’in vizyonu gerçekleşirse, 50 yıl sonra mezun öğrencilere matematiğin öğretilme şeklinin bugün olduğundan çok farklı olabileceğini söylüyor. “Gelecekte onun fikirlerinden etkileneceğini düşündüğüm birçok matematik alanı var” diyor.

Şimdiye kadar, bu vizyonun çoğu, Scholze ve Clausen bile doğru olduğundan emin olamayacak kadar ilgili teknik bir kanıta dayanıyordu. Ancak bu ayın başlarında Scholze, özel bilgisayar yazılımı kullanarak ispatın kalbini kontrol etme projesinin başarılı olduğunu duyurdu.

Bilgisayar yardımı

Matematikçiler, sayısal hesaplamalar yapmak veya karmaşık formülleri manipüle etmek için uzun süredir bilgisayarları kullandılar. Bazı durumlarda, bilgisayarların büyük miktarda tekrar eden iş yapmasını sağlayarak önemli sonuçlar elde ettiler – en ünlüsü 1970’lerde herhangi bir haritanın sadece dört farklı renkle ve herhangi iki komşu ülkeyi aynı renkle doldurmadan renklendirilebileceğinin kanıtıydı. renk.

Ancak kanıt asistanları olarak bilinen sistemler daha derine iner. Kullanıcı, makinenin zaten bildiği daha basit nesnelere dayalı bir matematiksel kavramın – bir nesnenin – tanımını öğretmek için sisteme ifadeler girer. Bir ifade aynı zamanda sadece bilinen nesnelere atıfta bulunabilir ve ispat asistanı, mevcut bilgisine dayanarak gerçeğin ‘açıkça’ doğru veya yanlış olup olmadığını cevaplayacaktır. Cevap açık değilse, kullanıcının daha fazla ayrıntı girmesi gerekir. İspat asistanları böylece kullanıcıyı argümanlarının mantığını titiz bir şekilde ortaya koymaya zorlar ve insan matematikçilerin bilinçli veya bilinçsiz olarak atladığı daha basit adımları doldururlar.

Araştırmacılar bir dizi matematiksel kavramı ispat asistanına çevirmek için çok uğraştıktan sonra, program diğer araştırmacılar tarafından üzerine inşa edilebilecek ve daha yüksek seviyeli matematiksel nesneleri tanımlamak için kullanılabilecek bir bilgisayar kodu kütüphanesi oluşturur. Bu şekilde, ispat yardımcıları, aksi takdirde bir insanın kontrol etmesi için zaman alıcı ve zor, hatta belki de pratik olarak imkansız olacak matematiksel ispatları doğrulamaya yardımcı olabilir.

Kanıt asistanlarının uzun zamandır hayranları var, ancak ilk kez bir alanın en uç noktasında büyük bir rol oynadıklarını söylüyor, diyor Imperial College London’da Scholze ve Clausen’in değerlerini kontrol eden bir işbirliğinin parçası olan matematikçi Kevin Buzzard. sonuç. “Kalan büyük soru şuydu: Karmaşık matematikle başa çıkabilirler mi?” diyor Buzzard. “Yapabileceklerini gösterdik”

Ve her şey herkesin hayal ettiğinden çok daha hızlı gerçekleşti. Scholze, Aralık 2020’de ispat asistanı uzmanlarına meydan okumasını ortaya koydu ve Almanya’daki Freiburg Üniversitesi’nde matematikçi olan Johan Commelin liderliğindeki bir grup gönüllü tarafından ele alındı. 5 Haziran’da – altı aydan kısa bir süre sonra – Scholze, Buzzard’ın blogunda deneyin ana bölümünün başarılı olduğunu bildirdi. Scholze, “Etkileşimli kanıt asistanlarının artık çok makul bir süre içinde zor orijinal araştırmaları resmi olarak doğrulayabilecekleri düzeyde olmasını kesinlikle çılgınca buluyorum” diye yazdı.

Scholze ve Clausen’e göre yoğunlaştırılmış matematiğin can alıcı noktası, modern matematiğin temel taşlarından biri olan topoloji kavramını yeniden tanımlamaktır. Matematikçilerin çalıştığı birçok nesnenin bir topolojisi vardır – nesnenin hangi parçalarının birbirine yakın olduğunu ve hangilerinin olmadığını belirleyen bir yapı türü. Topoloji bir şekil kavramı sağlar, ancak tanıdık, okul düzeyindeki geometriden daha dövülebilir bir kavramdır: topolojide, bir nesneyi parçalara ayırmayan herhangi bir dönüşüm kabul edilebilir. Örneğin, herhangi bir üçgen topolojik olarak diğer herhangi bir üçgene – hatta bir daireye – eşdeğerdir, ancak düz bir çizgiye değil.

Topoloji sadece geometride değil, aynı zamanda fonksiyonel analizde, fonksiyonların incelenmesinde de çok önemli bir rol oynar. Fonksiyonlar tipik olarak sonsuz sayıda boyuta sahip (kuantum mekaniğinin temelini oluşturan dalga fonksiyonları gibi) uzaylarda ‘yaşar’. olarak adlandırılan sayı sistemleri için de önemlidir. p– egzotik, ‘fraktal’ bir topolojiye sahip adic sayılar.

Büyük bir birleşme

2018 civarında, Scholze ve Clausen topoloji kavramına geleneksel yaklaşımın bu üç matematiksel evren – geometri, fonksiyonel analiz ve p-adic sayılar – ancak bu alternatif temeller bu boşlukları kapatabilir. Görünüşe göre tamamen farklı kavramlarla ilgilenseler de, bu alanların her birinde birçok sonucun diğerlerinde benzerleri var gibi görünüyor. Ancak bir kez topoloji ‘doğru’ bir şekilde tanımlandığında, teoriler arasındaki analojilerin aynı ‘yoğunlaştırılmış matematiğin’ örnekleri olduğu ortaya çıkıyor, iki araştırmacı önerdi. Clausen, “Bu, üç alanın bir tür büyük birleşimidir” diyor.

Scholze ve Clausen, bir dizi derin geometri gerçeğinin daha basit, ‘yoğunlaştırılmış’ kanıtlarını bulduklarını ve şimdi daha önce bilinmeyen teoremleri kanıtlayabileceklerini söylüyorlar. Bunları henüz kamuoyuna açıklamadılar.

Ancak bir nokta vardı: Geometrinin bu resme uyduğunu göstermek için, Scholze ve Clausen, düz bir çizginin topolojisine sahip olan sıradan gerçek sayılar kümesi hakkında oldukça teknik bir teoremi kanıtlamak zorunda kaldılar. Commelin, “Gerçek sayıların bu yeni çerçeveye girmesine izin veren temel teorem gibi” diye açıklıyor.

Prova yardımcısı yazılımı tarafından oluşturulan renk kodlu matematiksel ifadeler ve tanımlardan oluşan bir ağı gösteren diyagram.

Prova yardımcısı paketi Lean’de, kullanıcılar, Yalın kitaplığında zaten bulunan daha basit ifadelere ve kavramlara dayalı matematiksel ifadeler girerler. Burada Scholze ve Clausen’in anahtar sonucu durumunda görülen çıktı, karmaşık bir ağdır. İfadeler renklerle kodlanmış ve matematiğin alt alanlarına göre gruplandırılmıştır.

Clausen, Scholze’nin ispat üzerinde nasıl ‘irade gücüyle’ tamamlanıncaya kadar durmaksızın çalıştığını ve bu süreçte birçok orijinal fikir ürettiğini hatırlıyor. Clausen, “Şahit olduğum en şaşırtıcı matematiksel başarıydı” diye hatırlıyor. Ancak argüman o kadar karmaşıktı ki, Scholze’nin kendisi, tüm girişimi geçersiz kılan ince bir boşluk olabileceğinden endişelendi. Clausen, “İkna edici görünüyordu, ancak çok yeniydi” diyor.

Bu işi kontrol etmek için yardım için Scholze, kanıta yardımcı bir yazılım paketi olan Yalın konusunda uzman olan bir sayı teorisyeni olan Buzzard’a döndü. Yalın, başlangıçta, bilgisayar kodunu hatalara karşı titizlikle kontrol etmek amacıyla Redmond, Washington’daki Microsoft Research’teki bir bilgisayar bilimcisi tarafından oluşturuldu.

Buzzard, Imperial’deki tüm lisans matematik müfredatını Yalın olarak kodlamak için çok yıllı bir program yürütüyordu. Ayrıca, 2018’de Scholze’nin Fields Madalyası kazanmasına yardımcı olan mükemmel boşluklar kavramı da dahil olmak üzere sisteme daha gelişmiş matematiği girmeyi denemişti.

Aynı zamanda bir sayı teorisyeni olan Commelin, Scholze ve Clausen’in kanıtını doğrulama çabasında başı çekti. Commelin ve Scholze, Yalın projelerini Sıvı Tensör Deneyi olarak adlandırmaya karar verdiler. saygı Her iki matematikçinin de hayranı olduğu progresif rock grubu Liquid Tension Experiment’e.

Ateşli bir çevrimiçi işbirliği başladı. Yalın konusunda deneyime sahip bir düzine kadar matematikçi katıldı ve araştırmacılar yol boyunca bilgisayar bilimcilerinden yardım aldı. Haziran ayı başlarında ekip, Scholze’nin kanıtının kalbini – onu en çok endişelendiren kısım – tamamen Yalın’a çevirmişti. Ve hepsi kontrol edildi – yazılım, kanıtın bu bölümünü doğrulayabildi.

Daha iyi anlama

Commelin, Scholze’nin kanıtının Lean versiyonunun, orijinal versiyondan 100 kat daha uzun olan on binlerce kod satırı içerdiğini söylüyor. “Yalnızca Yalın koda bakarsanız, kanıtı, özellikle şimdi olduğu şekliyle anlamakta çok zorlanacaksınız.” Ancak araştırmacılar, kanıtın bilgisayarda çalışmasını sağlama çabasının onu daha iyi anlamalarına da yardımcı olduğunu söylüyorlar.

Riehl, ispat yardımcılarıyla deneyler yapan ve hatta bazı lisans derslerinde onlara öğreten matematikçiler arasındadır. Bunları araştırmalarında sistematik olarak kullanmasa da, matematiksel kavramları oluşturma ve bunlarla ilgili teoremleri ifade etme ve kanıtlama uygulamalarına ilişkin düşüncelerini değiştirmeye başladıklarını söylüyor. “Önceden, iki farklı şey olarak kanıtlamayı ve inşa etmeyi düşündüm ve şimdi onları aynı düşünüyorum.”

Pek çok araştırmacı, yakın zamanda matematikçilerin yerini makinelerin alma ihtimalinin düşük olduğunu söylüyor. Buzzard, ispat asistanları bir matematik ders kitabını okuyamaz, insanlardan sürekli girdiye ihtiyaç duyarlar ve matematiksel bir ifadenin ilginç mi yoksa derin mi olduğuna karar veremezler – sadece doğru olup olmadığına karar verirler. Yine de bilgisayarlar, matematikçilerin fark edemedikleri bilinen gerçeklerin sonuçlarını yakında gösterebilecekler, diye ekliyor.

Scholze, kanıt asistanlarının ne kadar ileri gidebileceğine şaşırdığını, ancak araştırmasında önemli bir rol oynamaya devam edip etmeyeceklerinden emin olmadığını söylüyor. “Şimdilik, bir matematikçi olarak yaratıcı çalışmalarımda bana nasıl yardımcı olacaklarını gerçekten göremiyorum.”

Profesör

Temel düzenleyici, farelerde progeria’yı tedavi eder

Previous article

BM Raporunda Dünya İçin Farklı Bir ‘Pandemi’ Türü Geliyor

Next article

You may also like

Comments

Comments are closed.

More in Gündem