Dolan kenar boşluğu

Anthropic'e göre şirketin Claude eylemcilerinden oluşan bir küme 11 gün boyunca kendi başına çalıştı ve Fermat'ın son teoremini, bir savın her adımını bilgisayara denetletebildiğiniz dil olan Lean'de yazılmış olarak getirdi. Şirket sonucu, yaklaşık 29.500 ara teoremi kapsayan 13 milyon satır olarak veriyor; bu, biçimselleştirilmiş matematiğin toplandığı ortak depo Mathlib'de biriken 2 milyon satırın beş katından fazla. Aynı işte beş yıllık bir insan çalışması yürüten Imperial College London'dan Kevin Buzzard, sonucun matematiğin aksiyomları dışında hiçbir varsayım bırakmadığını söyledi.[1]

Bunun ne kazandırdığını hatırlamakta yarar var. Andrew Wiles kanıtını 1993'te duyurdu, bir okur içinde bir kusur buldu ve o kusuru onarmak kendisiyle Richard Taylor'ın yaklaşık bir yılını aldı. Bir kanıt yardımcısı, türetemediği adımı geçirmiyor; dolayısıyla buradaki değişim savın ne söylediğine değil, sava kimin kefil olabileceğine uzanıyor. Fermat'ın iddiası geçen hafta bu saatlerde de doğruydu, bugün de doğru. Yeni olan, bir makinenin bütün yolu yürümüş ve eksik bir şey bulmamış olması.[1]

Makinenin yine de ihtiyaç duyduğu şey

Bunu aynı haftadan daha küçük bir sonucun yanına koyun. On beş yıl önce Eric Harshbarger'dan, kaç oyuncu olursa olsun sırayı adil biçimde ve berabere kalmadan belirleyecek zarlar istenmişti. Kendisi ve çevresindeki gevşek grup üç ve dört oyunculu durumları çözdü, sonra durdu. Harshbarger taradıkları uzayı yaklaşık 10 üzeri 128 dizilim olarak veriyor; hiçbir hesaplama gücü bu kadar seçeneği tek tek deneyerek bitiremez. Yanıt 2023'te Kanada'daki yazılım mühendisi Paul Meyer'den geldi; programı, grubun dört oyunculu veride çoktan bulduğu örüntüleri işledi: 1'den 300'e kadar her sayıyı taşıyan 60 yüzlü beş zar.[2]

İki hikâyenin biçimi ortak. Her ikisinde de makine, insanlar yapıyı sağladıktan sonra devreye girdi. Eylemciler Fermat'ın teoremine giden yolu bulmadı; Wiles ile Taylor'ın çoktan tamamladığı yolu biçimselleştirdi. Meyer'in programı arama uzayını geçip gitmedi; grubun dört oyunculu örüntülerle o uzayda açtığı kapıdan girdi. Bunun daha alçakgönüllü bir okuması var ve söylenmeyi hak ediyor: fark yalnızca her işe düşen hesaplama gücünde olabilir, çünkü biçimselleştirmenin satır satır izleyeceği yazılı bir sav vardı, zar aramasının ise yoktu. Yine de önümüzdeki kanıta bakılırsa iki makine de insan yapımı bir zeminden başladı.[1], [2]

Onu ortak zemine ne dönüştürür?

Bu köşe iki gün önce bir meyve sineğinin tamamlanmış sinir sistemine bakmış ve eksiksiz bir haritanın, davranışa dair tartışmayı bir arama işlemine çevirdiğini savunmuştu (Bir haşhaş tohumu kadar beyin, artık uçtan uca okunabiliyor). Aynı sınama şimdi matematiğe geliyor ve burada daha zor. Harita danışılmak için yapılır; 13 milyon satır Lean ise önce güvenilmek, sonra yeniden kullanılmak için. Bu büyüklükte bir ürün, ancak başkaları üzerine bir şey kurabildiğinde yerini hak ediyor. Buzzard'ın, yol boyunca üretilen cebir, harmonik çözümleme, geometri ve sayılar kuramı parçalarını üzerine bir şey kurulacak kadar sağlam bulurken işaret ettiği de buydu.[1], [3]

Yani izlenecek yalın bir şey var ve bunun için kimsenin bu işin nereye varacağını tahmin etmesi gerekmiyor. Biçimselleştirme önümüzdeki altı ay içinde Mathlib'e katılır ya da yeni Lean projelerince içeri alınırsa, bu ürünlerin üzerine bir şey kurulacak kadar sağlam olduğu iddiası ölçülebilir bir dayanağa kavuşacak; deponun bugün taşıdığı 2 milyon satır da ölçüt olacak. Ayrı durur, beğenilip kullanılmazsa, tek bir şirketin eylemcilerinin 11 günde neler yapabildiğine dair tek bir gösteri olarak kalır. Her durumda, Fermat'ın dar bulduğu kenar boşluğunda artık 13 milyon satır var ve hiçbiri ona ait değil.[1]