Matematik teoremlerini sağlam bir şekilde doğrulamak ve mantıksal kusurları ortaya çıkarmak için tasarlanan bir bilgisayar dili, bir fizik makalesine dönüştürüldü ve bir hata tespit edildi. Keşif, başka kaç makalenin benzer sorunları barındırabileceğine dair soruları gündeme getiriyor
Makineler matematiksel hataların tespit edilmesine yardımcı olabilir
Matematik teoremlerindeki hataları tespit etmek için oluşturulan bir bilgisayar dili, ilk kez çokça alıntı yapılan bir fizik makalesindeki temel bir hatayı ortaya çıkardı. Keşfin arkasındaki araştırmacı, bunun bu şekilde analiz ettiği ilk fizik makalesi olduğunu söylüyor ve bu da endişe verici bir soruyu gündeme getiriyor: Kaç tanesi hata içeriyor?
Matematikçilerin, formalizasyon olarak bilinen bir süreci kullanarak kanıtlarının doğru olduğunu, çelişkilerden ve mantıksal boşluklardan arınmış olduğunu kontrol etmelerine yardımcı olmak için özel yazılımlar giderek daha fazla kullanılıyor. Hatta bu yaklaşım, uzmanların yıllardır tartıştığı Shinichi Mochizuki’nin ABC varsayımı için 500 sayfalık geniş kapsamlı kanıtı gibi matematikteki en çetrefilli problemlerin bazılarına potansiyel bir çözüm olarak bile sunuldu.
Şimdi, Birleşik Krallık’taki Bath Üniversitesi’nden Joseph Tooby-Smith, Yalın adı verilen bir biçimlendirme dilini fizik alanına dönüştürdü. İki Higgs ikili modeli (2HDM) potansiyelinin kararlılığı üzerine 2006’da yayınlanan araştırmayı resmileştirmeye çalıştı; bu, o zamandan beri yaygın olarak alıntılandı, ancak tesadüfen teoremi baltalayan bir hatayı ortaya çıkardı.
Biçimselleştirilmiş teoremler, daha karmaşık teoremleri biçimlendirmek için yapı taşları olarak kullanılabilir ve Tooby-Smith, çalışmasının, MathsLib adı verilen matematik için yerleşik bir veri tabanı üzerine modellenen PhysLib adlı daha büyük bir biçimlendirilmiş fizik araştırması projesine makaleyi eklemek için bir “onay kutusu alıştırması” olması gerektiğini söylüyor. Tooby-Smith, “Oraya makaleleri çürütmek için gitmiyoruz; herkesin kullanabileceği sonuçlar oluşturmak için çıkıyoruz” diyor.
Hata, orijinal yazarların belirli bir C koşulunun problemin istikrarlı bir çözümü için yeterli olduğunu söylediği bir ifadeyle ilgilidir. Ancak Tooby-Smith, formalleştirme sırasında istikrarlı bir çözüm sağlamayan bir C koşulunun olduğunu gösterdi.
Tooby-Smith, hatanın keşfedilmesinin makale üzerinde çarpıcı bir etki yarattığını, ancak bunun üzerine inşa edilen ve alıntı yapılan çalışmalarda alt kademelerde sorunlara yol açmasının pek olası olmadığını söylüyor. Ancak artık birçok fizik makalesinin benzer hatalar içermesinden korkuyor ancak sorunun ne kadar geniş kapsamlı olabileceğinden emin değil. Bunun, resmileştirmenin yeni araştırma yayınlamanın standart bir parçası haline gelmesi için güçlü bir kanıt oluşturduğunu düşünüyor.
Tooby-Smith, fizikçilerin teoremlerde matematikçiler kadar açık ayrıntı vermeme eğiliminde olduklarını söylüyor. “Çünkü pek çok fizikçi bu ince ayrıntılarla ilgilenmiyor, bazen bunları gözden kaçırıyorlar ve işte bu noktada hata yapıyorsunuz” diyor.
Imperial College London’dan Kevin Buzzard, formalizasyonun matematik üzerinde büyük bir etkisi olduğunu ve en azından teorik fiziğin aynı şekilde ele alınmaması için hiçbir neden olmadığını söylüyor. “Böyle bir matematik yapmaya çalıştık ve gerçekten ilginç olduğu ortaya çıktı” diyor.
Ancak matematikte formalleştirmenin gerçek faydası artık mevcut resmileştirilmiş teoremlerin geniş bir külliyatından geliyor; bu, insan matematikçilerin bunların üzerine daha kolay inşa etmesine ve ayrıca yeni teoremleri daha hızlı resmileştirmeye yardımcı olabilecek yapay zeka modellerini eğitmesine olanak tanıyor. Matematiği resmileştirmek için bu yapay zeka modellerini eğitmek zaman aldı ve eğitim verileri olarak kullanılacak çok sayıda somut örnek vardı; bunlar henüz fizik için mevcut olmayabilir.
“İdeal olarak, bir milyon satırlık fiziğe ihtiyacımız var ve bunu elde etmek zor bir iş olabilir. Eğer makineler başlangıçta fizik yapmakta pek iyi değilse, o zaman başlangıçta manuel iş olacak ve sonunda makinelerin işi devralacağını umuyoruz” diyor Buzzard.
Orijinal fizik makalesinin yazarları, yorum talebine yanıt vermedi. Yeni Bilim Adamıancak Tooby-Smith, keşfi hakkında onları bilgilendirdiğini, kabul ettiklerine dair onay aldığını ve kendisine bir düzeltme yazısının yayınlanacağının söylendiğini söylüyor.
