Hobici, bir aylık Claude iş birliğinin Conway'in 1976 varsayımının Lean ispatını verdiğini iddia ediyor

Yazarın iddiası

Kendini "matematik çaylağı" olarak tanımlayan bir kişi, yaklaşık elli yıl önce John Conway'in süreal sayılar hakkında ortaya attığı bir varsayımın makine tarafından doğrulanmış bir Lean ispatını üretmek için uç bir yapay zekâ modeli kullandığını söylüyor. overreacted.io'da yazan ve Hacker News'in ana sayfasına ulaşan bir gönderide yazar, projenin bir aylık boş zaman ve ciddi miktarda token ile tamamlandığını bildiriyor.

Sonuç henüz doğrulanmış değil. Yazar, hiçbir matematikçinin ispatı bağımsız olarak doğrulamadığını açıkça belirtiyor. Gönderiye göre ispatı destekleyen şey, Palomar kayıt defterinin yürüttüğü mekanik kontrollerden geçmek ve hem Lean'i hem de bu alanı bilen birkaç kişiden, biçimlendirilmiş ifadenin varsayımı doğru şekilde yansıttığına dair gayri resmi güvence. Lean çekirdeğinin kendisinde bir hata olmadığı sürece, ispatın büyük olasılıkla meşru olduğunu savunan yazar, açıkça çürütülmeye davet ediyor.

Hedef aldığı varsayım

Conway'in icadı olan süreal sayılar, tüm gerçel sayıları, tüm ordinal sayıları (sonsuz büyük ω, ω + 1, ω × ω) ve 75 + 3ω + 1/ω gibi daha tuhaf karışımları içeren bir sayı sistemi oluşturur. Bunların çekici yanı — özellikle bir programcının gözünde — tüm bu evrenin tek bir kuraldan büyümesidir: her adımda, elinizdeki sayılar arasındaki her boşlukta yeni bir sayı yaratın — iki taraftaki her şeyin ötesindeki boşluklar dahil — ve sonsuza dek tekrarlayın.

Omnific tam sayıları, bu evrenin tam sayıya benzeyen parçasıdır. 3 ve –5 gibi sıradan tam sayıları içerirler ama ω, ω × ω ve –ω/7 gibi sonsuz "bütün" sayıları da.

Conway'in 1976 tarihli arıtma varsayımı, bu tam sayıların sıradan tam sayılarda理所 tabi saydığımız bir özelliği koruduğunu söyler. Sıradan tam sayılarda 10 × 21, 6 × 35'e eşittir çünkü çarpanlar yeniden düzenlenebilir: 10 = 2 × 5 ve 21 = 3 × 7, 2 × 3 = 6 ve 5 × 7 = 35 olarak yeniden birleştirilebilir. Conway, aynı şeyin omnific tam sayıları için de işe yaradığını varsaydı: ab = cd olduğunda her zaman a = ef, b = gh, c = eg ve d = fh olacak şekilde e, f, g, h bulunmalıdır.

Proje nasıl gelişti

Yazarın yöntemi, modele yön vermeye izin vermekti. Önce Claude'dan süreal sayılar alanındaki açık bir problem seçmesini istediler. Okuma ve daraltma seanslarının ardından model, Conway aritmetiğini seçti — özellikle belirli bir seri halkası olan K((ℝ^≤0)) içinde sonsuz destekli her indirgenebilirin asal olup olmadığı sorusunu. L'Innocente ve Mantova'nın yakın tarihli çalışması, Conway'in 1976 varsayımını tam olarak bu soruna indirgemişti. Claude ayrıca 2026'ın Conway'in On Numbers and Games kitabının ellinci yılı olduğuna dikkat çekti; bu da seçimi duygusal olarak cazip kıldı — ancak yazar, bunun Conway'in kendi varsayımlarından ayakta kalan sonuncusu olduğu yönündeki model iddiasını doğrulayamadığını itiraf ediyor.

Yola çıkmadan önce tek bir ön koşul kontrol edildi: varsayımın Lean'de öz biçimde ifade edilebilmesi. Yazarın mantığına göre bu olmadan, ispat doğru olsa bile kimseye inceletmek imkânsız olurdu.

Erken denemeler kötü şekilde başarısız oldu. Yazar, Claude'dan varsayımı ispatlamasını ya da yapılandırılmış bir karşı örnek aramasını istedi, ilgili makaleleri modele PDF'leri tekrar tekrar çözmek zorunda kalmaması için TeX'e dönüştürdü ve gerektiği kadar zaman ve işlem gücü harcaması için onu teşvik etti. Yazarın yazdığına göre bu aşamadaki çıktıların çoğu, gerçek bir ilerleme değil, işi gerekçelendirmek için uydurulmuş yoğun ve etkileyici görünen metinlerdi — yine de o seanslardaki birkaç fikir nihai argümana katkı vermiş olabilir. Başka bir deyişle sonuç, tek bir prompt'tan değil, bir aylık yinelemeden geldi.

Neden önemli

Bu, alan uzmanlığı olmayan insanlar için uç modellerin matematik iş birlikçisi olarak ne yapabildiğine dair el yordamıyla elde edilmiş bir veri noktası; hem de yapay zekâ matematik sonuçlarının manşetlere taşındığı ve "bir atılım yap"ın sosyal medya meme'ine dönüştüğü bir yılda geliyor. Lean ile biçimlendirme ayrıca bir ispatına inanmanın ne gerektirdiğini de değiştiriyor: güven, yazarı incelemeden, biçimsel ifadenin varsayımla eşleşip eşleşmediğini ve doğrulayıcının kendisinin sağlam olup olmadığını incelemeye kayıyor.

Sınırlar da en az kadar öğretici. İspat bağımsız insan doğrulamasını bekliyor, doğruluğu ifadenin sadakatle biçimlendirilmiş olmasına ve Lean çekirdeğinin hatasız olmasına dayanıyor ve naif tek atımlık prompt'lar kullanılabilir hiçbir şey üretmedi. Yapay zekâ destekli matematiğin nerede durduğunun bir sinyali olarak bu hikâye, modellerin açık problemleri tek başına çözdüğünden çok, kararlı bir meraklının artık ciddi ciddi neyi deneyebildiğiyle ilgili — ve darboğaz olarak üretim değil, doğrulama geriye kalıyor.