AI destekli Lean ispatı, 11 karenin optimal dizilimini doğruladı

11SquaresFormalized adlı bir GitHub deposu, on bir eş kareyi mümkün olan en küçük kare konteynera dizme probleminin en iyi olma kanıtının eksiksiz bir Lean formalizasyonunu yayımladı. Bu çalışma, "AI-assisted proof of optimal packing for 11 squares" başlığıyla Hacker News'in ana sayfasına yerleşti ve depoya göre yapılan bir dış doğrulama çalışması, 7.920 yerel Lean modülünün tamamını kabul eden ve hiçbir şeyin denetlenmeden kabul edilmediğini raporlayan nihai bir denetimle sonuçlandı.

Teorem ne diyor

Sonuç, on bir küçük kareyi barındırabilecek bir karenin en küçük kenar uzunluğunu, README'de kasıtlı olarak esnek biçimde tanımlanan bir model altında sabitliyor: kareler yalnızca eksenlere hizalı olmak zorunda değil rastgele yönelimlerde bulunabilir, sınır ve birbirleriyle yasal temasta bulunabilir ve açık iç kısımları ayrık kalmalıdır.

Optimal kenar uzunluğu tam olarak (6u+4)/(1+2u-u^2) biçiminde ifade edilir; burada u, sekizinci dereceden 5u^8 - 10u^7 - 2u^6 + 14u^5 + 12u^4 - 6u^3 + 2u^2 + 2u - 1 = 0 polinomunun 9/25 ile 37/100 arasındaki tek köküdür. Sayısal olarak, sınırı gerçekleştiren yapı yaklaşık 3.8770835900228141773 ölçüsündedir. Ana ifadeler — koşulsuz en iyi olma ve bir kenar uzunluğu alt sınırı — ElevenSquare/Optimality.lean dosyasında yer alır; bu kamusal hedeflere yönelik aksiyom sorguları ise ElevenSquare/Verification.lean dosyasındadır.

Kanıt nasıl inşa edildi

Kanıt, katmanlı bir kod tabanına yayılıyor. ElevenSquare/Foundations.lean dosyası geometriyi, kesin bir uç noktayı, sınırı gerçekleştiren yapıyı, kapalı hücreli bir örtüyü ve sonlu sayıda vakaya bir indirgemeyi içeriyor. Tasks ve Sqpack dizinleri geometrik argümanları, sertifika denetleyicilerini, üretilmiş kanıtları, sadeleştirmeleri ve yerel analitik çalışmayı barındırırken, Pending adlı bir dizin, artık entegre kanıt tarafından karşılanan özgün kamusal arayüzleri koruyor — README'nin belirttiğine göre ad tarihsel.

Yeniden üretilebilirlik için her şey sabitlenmiş durumda. Depo, kanıt kaynaklarını ve yapılandırmasını 1bf942a7af1ea330e95489d8997deebd4227ca71 commit'inden içe aktarıyor, Lean 4.34.1 üzerinde çalışıyor ve Mathlib'in d13f23b723b8a846827a245b89c10fc7d3f11612 revizyonunu sabitliyor.

Neyi güvenilir kabul ediyorsunuz

README, güven modeli konusunda alışılmadık ölçüde açık. Seçili maliyetli, kesin sayısal sertifika kontrolleri native_decide kullanılarak karşılanıyor; dolayısıyla nihai teorem, Lean çekirdeğine ek olarak yerel derleyiciye de dayanıyor — ve proje bunun yalnızca çekirdek temelli bir doğrulama iddiası olmadığını açıkça belirtiyor. Sıradan Lean kanıtları geometriyi, denetleyici sağlamlığını ve nihai teoremin birleştirilmesini kapsamaya devam ediyor ve onaylanan her sayısal bildirim, kesin kaynak karmasıyla birlikte verification/native-certificates içinde kayıt altına alınıyor; böylece genişletilmiş güvenilir yüzey küçük ve denetlenebilir kalıyor.

Çalışmayı yeniden üretmek

Doğrulama betiklerle yürütülüyor. Linux'ta, Python 3, Git, curl ve tar mevcutken scripts/run_verification.sh --bootstrap --jobs 2 komutunu çalıştırmak sabitlenmiş araç zincirini hazırlar ve her şeyi seri biçimde derler; macOS kullanıcılarının önce elan başlatıcısını kurması gerekir. Komut her yerel modülü denetler ve ardından nihai bir kaynak, makbuz, bağımlılık ve aksiyom denetimi gerçekleştirir. Gerçek bir başarı üç koşulun birlikte sağlanmasını gerektirir: OPTIMALITY_PROVED_WITH_NATIVE_CERTIFICATES bayrağı, hiçbir şeyin kabul edilmediği bir denetim ve nihai sonuçta trust_model: lean_kernel_and_native_compiler — yalnızca modüllerin yüzde 100'ünü derlemek tek başına açıkça yeterli değildir. Daha hafif bir seçenek olan scripts/check_sources.py, kaynakları Lean'e hiç başvurmadan doğrular.

Sürüme iki uyarı eşlik ediyor. Başarılı kaynak çalışması EvolvingPrograms'ın daha büyük koşucusunu kullandı; bu yüzden proje soğuk derleme süresi belirlemiyor veya macOS'ta iki-üç saatlik bir çalışmayı garanti etmiyor. Ve README, bu anlık görüntüde geçmiş materyalistleştirme komutlarının veya verify.py --setup komutunun çalıştırılmamasını öneriyor; çünkü bunlar yerini almış üretilmiş kaynakları geri yüklerdi.

Neden önemli

Kare dizimi, küçük vakaların bile karmaşık argümanlar gerektirebildiği klasik bir geometrik eniyileştirme problemidir ve en iyi olma iddiaları tarih boyunca elle doğrulanması zor olmuştur. Makine denetimli bir kanıt yükü yerinden oynatır: okuyucuların yazarların cebirine değil, yalnızca sabitlenmiş anlık görüntüden herkesin yeniden çalıştırabileceği küçük ve incelenebilir bir araç zincirine güvenmesi yeterlidir.

Proje ayrıca dürüst bir güven muhasebesi modeli sunuyor. Garantilerini abartmak yerine, hangi sayısal kontrollerin Lean çekirdeği dışında kaldığını tam olarak beyan ediyor ve ilgili bildirimlerin karmalarını yayımlıyor. Bu disiplin, yapay zekâ sistemleri formal kanıtları oluşturmada daha büyük bir rol üstlendikçe daha da önem kazanıyor — bu çalışmanın Hacker News'te AI destekli olarak çerçevelenmesi ile EvolvingPrograms, @ctjlewis ve diğer katkıcılara verilen atıflar birlikte makul bir iş bölümü çiziyor: makineler ve yapay zekâ araçları devasa bir kanıtı inşa etmeye ve üzerinde yinelemeye yardımcı olurken, gerçek matematiksel garantiyi bağımsız bir doğrulayıcı ve yeniden üretilebilir bir denetim sağlıyor.