Lean4, Terence Tao’nun son makalesindeki küçük bir hatayı bulmaya yardımcı oldu

• Terence Tao’nun mathstodon.xyz gönderisi
• Terence Tao’nun son makalesinde, Lean4 biçimselleştirme projesi sayesinde küçük ama önemli bir hata bulundu
• Hata, makalenin 6. sayfasında biçimselleştirme sürecinde bulundu; makaleye https://arxiv.org/pdf/2310.05328.pdf adresinden ulaşılabilir
• Tao’nun makalesinde, n=3, k=2 durumu için ıraksayan 12log⁡n−1n−k−1 ifadesi tespit edildi
• Sorun yalnızca n’nin küçük değerlerinde ortaya çıkıyor ve sayfadaki bazı sayısal sabitlerin değiştirilmesiyle çözülebiliyor
• n≥8 durumunda mantık hâlâ geçerli; küçük n değerleri içinse daha basit bir yöntem kullanılabiliyor
• Lean4, Tao’dan 0<n−3 ifadesini kanıtlamasını istedi, ancak elinde yalnızca n>2 varsayımı vardı; bu da bir çelişkiyi ortaya çıkardı
• Tao, Lean4’te biçimselleştirmeyi denedikten sonra fark edilen bu küçük hatayı kabul eden bir dipnotu makalenin yeni sürümüne eklemeyi planlıyor
• Bu gönderi, topluluğun ilgisini ve olumlu tepkisini çekerek, gelecekteki çalışmalar için sağlam bir temel oluşturmada ispat yardımcılarının önemini vurguluyor

[GN⁺]

Hacker News görüşü

• Ünlü matematikçi Terence Tao, Lean4 ve GPT4 kullanarak yakın tarihli bir makalesindeki küçük bir hatayı buldu.
• Tao'nun Lean4 öğrenme süreci Mastodon gönderilerinde kayıt altına alındı ve bu da Lean4'ün çalışmayı nasıl hızlandırabildiğine dair ilginç bir vaka incelemesi oluşturdu.
• Yeni başlayanlara, Lean4'e kolay bir giriş olarak Natural Number Game tavsiye ediliyor.
• Bir kullanıcı, Lamport'un TLA+ aracını kullanarak biçimsel belirtimler oluşturma ve programlamadaki hataları azaltma deneyimini paylaştı.
• Derleyicide uygulanmasının getirdiği karmaşıklığa rağmen, bağımlı tiplere ilgi var.
• Lean4 ile otomatik ispatın birleşimi, gelecekte umut vadeden bir teknoloji kombinasyonu gibi görünüyor ve yeni keşifleri teşvik etme potansiyeli taşıyor.
• Tao'nun Lean öğrenmek için Copilot kullanması, Lean4'ün yeni araçları benimsemedeki sürtünmeyi nasıl azaltabileceğine dair bir örnek olarak öne çıkarıldı.
• Tao'nun Lean4 ile ilgili ilerlemesi GitHub hesabında görülebilir.
• Bir kullanıcı, biçimsel ispat denetleyicileri ile dil modellerini birleştirerek sentetik varsayım-ispat çiftleri üretme fikrini önerdi; bunun ispat üretiminde insanüstü yeteneklere kadar ölçeklenme potansiyeli olabilir.
• "Bug" terimi, matematiksel bir hatayı açıklamak için kullanıldı ve bazı kullanıcılar bunu alışılmadık buldu.