Araştırma AI Minute Newsroom 2026-08-20

Makine yazımı ispatlar o kadar çoğaldı ki matematikçiler bir kayıt bürosu kurdu — iki denetiminden birini bir dil modeli yapıyor

Terence Tao 18 Ağustos'ta, Lean FRO ve ICARM tarafından kuluçkaya alınan Lean doğrulamalı matematik kayıt sistemi Palomar'ın gönderime açıldığını duyurdu. Çözmeye çalıştığı sorun yeni: son aylarda eski ve yeni sonuçların yapay zekâ üretimi ispatları büyük sayıda ortaya çıktı ve bunların hatırı sayılır bir kısmı, her adımı makineye onaylatmayı sağlayan ispat asistanı Lean'de biçimselleştirildi. Ama GitHub'da duran bir Lean deposu kendi kendini anlatmaz. Kodun, yazarının iddia ettiği şeyi gerçekten ispatlayıp ispatlamadığını çıkarmak ciddi bir emek ister; Lean kullanmayan bir matematikçi için neredeyse imkânsızdır. Palomar, gönderilen depoyu iki denetimden geçiriyor. İlki mekanik: Comparator adlı Lean aracı, modülün tip denetiminden geçtiğini ve tam olarak iddia edilen sonuçları ispatladığını doğruluyor. İkincisi, gündelik dildeki açıklamanın biçimsel ifadeyle örtüşüp örtüşmediğini soruyor ve bu denetimi büyük bir dil modeli yapıyor. İkisini de geçen depolar kayda alınıyor; tam ifade, dayanılan kütüphaneler ve değerlendirenin notları yanında yayımlanıyor. Tao bunu Lean ispatları için bir ön baskı sunucusunun karşılığı diye tanımlıyor ve Jeremy Avigad, Matthew Ballard, Jaume de Dios, Nestor Guillen, Bryna Kra, Kim Morrison, Ravi Vakil ve Akshay Venkatesh ile birlikte bilimsel danışma kurulunda yer alıyor.

Bu neden önemli?Matematikte hakem değerlendirmesi iki ucunda da insan darboğazı varsayıyordu: bir kişi ispatı yazar, insanlar okur. Makineler ilk yarıyı kırdı; ikinci yarı zaten hiç ölçeklenmemişti. Palomar, eksik tesisatı kurmaya yönelik ilk ciddi girişim ve merkezindeki tavizi açıkça söylüyor. Biçimsel denetim su sızdırmaz; ama biçimsel ifadenin gerçekten kimsenin umursadığı ifade olup olmadığı sorusunu, tam da bu selin sebebi olan türden bir sistem cevaplıyor. Bu bir skandal değil, elde olan dürüst seçenek ve gizlenmek yerine açıkça yazılmış. Daha büyük işaret şu: bir disiplin, makine üretimi işi kabul edip etmeyeceğini tartışmayı bırakıp onu ayıklayacak altyapıyı tasarlamaya başladı. Bu, hemen hemen her başka alandan daha ileri bir nokta.

#Kodlama #Bilim & Araştırma

✓ Doğrulandı · 4 kaynak

Uygulamada oku — ücretsiz, 9 dilde

İlgili haberler

ABD, 16 ülkeyi bilimin merkezine yapay zekâyı koymaya ikna etti.
2026-10-05 OpenAI 28 gün boyunca her gün ya yenilik ya kota sıfırlaması verecek.
2026-10-05 Matematikçiler beş açık problemi sıradan bir sohbet kutusuyla çözdü.
2026-10-05 Ham modeller, cilalı sürümlerinin çözemediği işleri çözdü.
2026-10-04 Google hata ödül programını yapay zekâ ihbarları yüzünden durdurdu.
2026-10-04