Claude eylemcileri Fermat'ın son teoremini 11 günde Lean'de biçimselleştirdi
Anthropic'e göre Claude eylemcileri, Wiles ile Taylor'ın mevcut Fermat kanıtını 11 günde Lean koduna çevirdi. Yaklaşık 29.500 ara önermeyi kapsayan 13 milyon satırlık biçimselleştirmede son mantık denetimini Lean yaptı. Çalışma, 1990'larda tamamlanan kanıtın her adımını bilgisayarın sınayabileceği biçime getiriyor; teorem için yeni bir çözüm sunmuyor.
Bilim··Gece
11 günde 13 milyon satırlık biçimselleştirme
Anthropic'in açıklamasına göre Claude eylemcilerinden oluşan bir küme, Fermat'ın son teoreminin kanıtını 11 gün içinde Lean dilinde biçimselleştirdi. Çıktı 13 milyon satır Lean koduna ulaştı ve son biçime giren yaklaşık 29.500 ara önermeyi kapsadı. Bu büyüklük, biçimselleştirilmiş matematiğin toplandığı Mathlib deposundaki 2 milyon satırın beş katından fazla. İki haber de süreyi ve son ürünün kapsamını aktarırken, MoneyToday çalışmada onlarca eylemcinin görev aldığını belirtiyor.[1], [2]
Yeni çözüm yerine mevcut kanıtın eksiksiz yazımı
Eylemciler teoremi yeni bir yoldan çözmedi. Andrew Wiles ile Richard Taylor'ın 1990'larda tamamladığı matematiksel kanıtı, Lean'in her adımı türetebildiği bir biçime çevirdi. Matematik metinleri uzmanların açık saydığı ara adımları atlayabilir; biçimselleştirme bu boşlukların da yazılmasını gerektiriyor. Wiles'ın 1993'te duyurduğu kanıtta daha sonra bir kusur bulunmuş, Wiles ile Taylor bu sorunu yaklaşık bir yılda onarmıştı. Yeni çalışmada son mantık denetimini başka bir yapay zekâ değil, Lean yaptı.[1], [2]
Büyük kanıt daha küçük önermelere ayrıldı
Çalışmada büyük kanıt, farklı eylemcilerin çözebileceği daha küçük önermelere ayrıldı; bir eylemcinin tamamladığı sonuç başka bir eylemcinin daha zor bir adımında kullanıldı. İnsan uzmanlar zaman zaman üst düzey yönlendirme yaptı. New Scientist'ın aktardığına göre eylemciler birkaç kez projenin durumunu izleyemez hale geldi. Ekip daha sonra, matematikçilerin birlikte çalışması için geliştirilmiş Prove2Me aracını kullandı. Süreç, cebir, harmonik çözümleme, geometri ve sayılar kuramına ait yeniden kullanılabilecek biçimsel parçalar da üretti.[1], [2]
İlgili köşe yazıları
Bu gündem hakkında daha fazla bilgi için ilgili köşe yazılarını okuyabilirsiniz.
