Erdős Problemi #728, yapay zeka tarafından neredeyse otonom biçimde çözüldü

• Erdős Problemi #728, yakın zamanda yapay zeka araçları tarafından neredeyse otonom biçimde çözülerek matematik araştırmalarının otomasyonunda yeni bir dönüm noktası oluşturdu
• Problem, başlangıçta Erdős, Graham, Ruzsa, Strauss tarafından 1975'te ortaya atılan, binom katsayılarının asal çarpanlara ayrılmasıyla ilgili bir soruydu; ancak muğlak koşullar nedeniyle uzun süre net biçimde ele alınamadı
• ChatGPT, ayarlanmış kısıtlar altında bir ispat üretti; Aristotle ise bunu Lean biçimsel ispatı olarak resmileştirip hataları otomatik olarak düzeltti
• Ardından çeşitli katılımcılar bunu ChatGPT kullanarak doğal dile yeniden yazdı ve literatür bağlantıları ile anlatı yapısını güçlendiren sürümleri yinelemeli olarak geliştirdi
• Terence Tao, bu sürecin yapay zekanın hızlı ispat yazma ve düzeltme yeteneğinin araştırma makalesi yazım biçimini bizzat değiştirme potansiyelini gösterdiğini değerlendirdi

---

Yapay zekanın çözdüğü Erdős Problemi #728

• Son dönemde yapay zeka araçlarının uygulanması, Erdős problemlerinin çözümünde yeni bir ilerleme gösterdi ve Problem #728 neredeyse otonom biçimde yapay zeka tarafından çözüldü
  • İlk denemenin ardından geri bildirim yansıtılarak düzeltilen sürümde başarı sağlandı
  • Sonuç, mevcut literatürde birebir yeniden üretilmiş değildi; yalnızca benzer yöntemlerle elde edilmiş yakın sonuçlar vardı
• Bu örnek, son birkaç ayda yapay zekanın matematiksel problem çözme yeteneğinin gerçekten geliştiğini gösteriyor
  • Geçmişte de yapay zekanın Erdős problemlerini çözdüğü örnekler olmuştu, ancak çoğu daha sonra literatürde zaten var olan çözümler çıktı
• Bu problemde, Erdős'ün özgün ifadesinin hatalı biçimde sunulduğu ve ancak yakın zamanda amaçlanan biçimde yeniden kurulduğu anlaşıldı
  • Bu durum, mevcut literatürde ilgili çalışmanın neden az olduğunu da açıklıyor

Problemin geçmişi ve ilk yaklaşım

• 1975'te Erdős, Graham, Ruzsa, Strauss, binom katsayısı (2n choose n) içindeki asal çarpanlara ayrılmayı incelerken çeşitli ilişkili problemler ortaya koydu
  • Bunlardan biri, a!b! | n!(a+b−n)! koşulunu ve a+b > n + C log n eşitsizliğini sağlayan sonsuz sayıda a, b, n bulunup bulunmadığını soruyordu
  • Ancak C'nin büyüklüğü (küçük mü büyük mü olduğu) gibi çeşitli noktalar belirsiz biçimde ifade edilmişti
• Birkaç ay önce AlphaProof ekibi problemin basit bir çözümünü buldu, ancak bunun problemin amaçlanan ruhuna uymadığı düşünülerek a,b ≤ (1−ε)n kısıtı eklendi
  • Sonrasında yapay zeka destekli literatür taramalarında da ilgili çalışma neredeyse hiç bulunmadı

ChatGPT ve Aristotle işbirliği

• 4 Ocak'ta ChatGPT, ayarlanmış kısıtlar altında küçük C durumu için bir ispat üretti
  • Bu ispat, Aristotle tarafından Lean biçimsel ispatına dönüştürüldü
  • Daha sonra özgün metin yeniden incelendiğinde, asıl makalenin zaten küçük C durumunu ele aldığı doğrulandı
• Başka bir katılımcı, Lean ispatını ChatGPT ile doğal dile dönüştürdü ve ek diyaloglarla iyileştirilmiş bir sürüm hazırladı
  • Bu sürüm bazı ispat boşluklarını doldurdu, ancak hâlâ yapay zekaya özgü bir miktar tuhaf üslup ve yetersiz literatür atfı barındırıyordu
  • Buna rağmen temel fikri anlamaya yetecek kadar okunabilir bir düzeye ulaştı

Büyük çaplı yeniden yazım ve iyileştirilmiş sonuç

• Ek istemlerle ChatGPT, ispatı büyük C durumunu da kapsayacak şekilde genişletti
  • Bazı hatalar vardı, ancak Aristotle bunları otomatik olarak düzeltti ve Lean tarafından doğrulanmış ispatı tamamladı
• Üçüncü bir katılımcı Lean ispatını sıkıştırdı; ardından başka bir katılımcı ChatGPT ile uzun süreli diyaloglar aracılığıyla
  • bunu literatür bağlantıları ve anlatı yapısı güçlendirilmiş, tamamlanmış bir makale formuna yeniden yazdı
  • Ortaya çıkan metin, yapay zeka üretimi hissi azalmış, araştırma makalesi düzeyine yaklaşan bir kalite olarak değerlendirildi
  • Tao, bu metni Erdős Problem Forumu'nda incelediğini belirtti

Yapay zekanın araştırma makalesi yazımını değiştirme biçimi

• Tao'ya göre nihai makalede çekirdek bölümlerin hâlâ insanlar tarafından yazılması gerekiyor, ancak
  • yapay zeka ile Lean'ın birleşimi, ispat yazımı ve düzeltme hızını çarpıcı biçimde artırdı
• Önceden bir makaleyi rahat okunur hale getirmek çok zaman alıyordu ve
  • hakem geri bildirimlerine göre yapılan düzeltmeler de çoğu zaman yerel değişikliklerle sınırlı kalıyordu
• Ancak artık yapay zekanın metin üretme ve düzeltme yeteneği ile biçimsel ispat araçlarının doğrulama işlevi birleşerek
  • farklı ayrıntı düzeyleri ve anlatım biçimleriyle makalenin yeni sürümlerini hızla üretmeyi mümkün kılıyor
• Tek bir “resmî makale”nin ötesinde, yapay zeka tarafından üretilmiş çok sayıda yardımcı sürümün var olması
  • çeşitli bakış açıları ve ek değer sunma potansiyeline işaret ediyor

Topluluk tepkisi

• Bazı kullanıcılar, yapay zeka tarafından üretilen belgelerin ek değerini “aynı şeye başka açılardan bakabilme yeteneği” olarak açıkladı
• Diğer matematikçiler ise yapay zeka sonuçlarının özgünlüğünü ölçme veya mevcut literatüre benzerliğini değerlendirme gereğini gündeme getirdi
  • Örneğin, Lean biçimsel ispat uzunluklarının karşılaştırılmasıyla nicel benzerlik ölçümü yapılması önerildi
• Başka bir yorumda, yapay zekanın kod refactoring'inde olduğu gibi makaleleri küresel ölçekte yeniden yazabileceği belirtilerek
  • araştırmacıların daha üst düzey belge yapısı tasarımına odaklanması gerektiği savunuldu
• Bazıları yapay zekanın matematikçilerin rolünü ikame etme olasılığına kuşkuyla yaklaşsa da
  • diğerleri bunu işbirliği ve düşünceyi genişletme için yeni bir fırsat olarak değerlendirdi

[GN⁺]

Hacker News görüşleri

• Harmonic'te çalışıyorum ve geliştirdiğimiz Aristotle hakkında bazı yanlış anlamaları düzeltmek istiyorum
  Aristotle, dil modellemeyi de içeren son teknoloji AI tekniklerini yoğun biçimde kullanıyor
  İngilizce yazılmış gayriresmî bir ispat girildiğinde, ispat doğruysa bunu Lean'a çevirme olasılığı yüksektir. Yani bu, İngilizce ispatın sağlam olduğuna dair güçlü bir sinyaldir
  Lean'da biçimselleştirildiğinde ise ispatın doğru olduğundan artık şüphe kalmaz. Temel yaklaşımımız bu — AI destekli arama ile cevabı bulduğumuzda, ne kadar karmaşık olursa olsun sonucun doğruluğunu garanti edebiliyoruz

  • AI'ın Lean'a çevirdiği ispatın gerçekten problemin doğru biçimselleştirmesi olduğunu nasıl doğruladığınızı merak ediyorum. Üretken AI'ın diğer alanlarda inandırıcı yalanlar üretmekte iyi olduğunu biliyoruz; burada da benzer bir risk olup olmadığını merak ediyorum
  • Bu teknolojiyi yazılım doğrulama için uygulamaya yönelik girişimler olup olmadığını merak ediyorum
    Rust, bellek güvenliğini garanti etmek için sabit bir kural kümesi kullanıyor, ancak bu kurallar basit ve kısıtlı. Eğer Aristotle benzeri bir sistem derleyiciye entegre edilip, kodun doğruluk ispatı mümkün olduğunda otomatik olarak geçmesine izin verebilse, gerçekten harika olurdu
  • Her yeni LLM çıktığında bunun gerçek bir ilerleme mi yoksa sadece benchmark hackleme mi olduğunu ayırt etmek zor oluyor; matematiksel ispatların biçimselleştirilmesinin ise gerçek ilerlemeyi gösteren bir ölçüt olduğunu düşünüyorum
    Harmonic'in insanlar tarafından yazılmış matematiğin büyük kısmını biçimselleştirebilmesi ne kadar sürer merak ediyorum. Rakipleri Christian Szegedy bunun bu yıl içinde mümkün olacağını söylüyordu
  • İngilizce ispat doğruysa Lean'a çevirme olasılığının yüksek olduğunu söylediniz; bunun matematiğin alana göre zorluk düzeyine bağlı olarak değişip değişmediğini merak ediyorum. Bildiğim kadarıyla hâlâ insanların bile biçimselleştirmekte zorlandığı pek çok araştırma alanı var
  • “Önerme doğru biçimselleştirildiyse” önkoşulu oldukça büyük bir varsayım gibi geliyor. Yakın zamandaki Navier-Stokes vakasında da gördüğümüz gibi, biçimselleştirmenin kendisi kolay değil

• Terence Tao'nun açıklamasına bakılırsa, bir insan iki AI aracı arasında sonuçları gidip getiriyor ve AI da insanın bulduğu boşlukları doldurma rolünü üstlenmiş gibi görünüyor
  Bu, tamamen otonom bir çözümden ziyade insan ile AI'ın iş birliğine daha yakın. Yani uzman yön veriyor, AI yardımcı oluyor

  • Evet, benim anladığım da Aristotle, ChatGPT ve çok yetenekli bir kullanıcının etkileşim içinde ilerlediği yönünde
  • Tao'nun ya da topluluğun boşlukları bizzat bulduğunu değil, otomatik ispat doğrulayıcısı kullandıklarını duymuştum. Hatta oran %90 AI / %10 insan gibi görünüyor
  • Yazarın ayrıntılı açıklaması Reddit'te var — Reddit gönderisi
  • İnsan uzmanlığının ve emeğinin düzeyini anlamak için Erdős Problem Forumu'ndaki başlığı okumanızı öneririm
  • Bu arada, bu site matematikçi Thomas Bloom tarafından yapıldı ve ChatGPT teknik kurulumda yardımcı oldu (SSS'den alıntı)

• Mevcut ispatları yeniden kurmak ya da yeni şekillerde birleştirmek insanlar için sıkıcı veya karmaşık bir süreç olabilir, ama AI bunu insanüstü hızlarda yapabilir
  Bu yaklaşım, AGI öncesi aşamada bile muazzam imkânlar açacaktır. Matematikçilerin AI'ı bir araç olarak kullanıp Milenyum Problemleri gibi zor sorularla uğraştığı bir döneme gireceğimizi düşünüyorum

  • Mevcut ispatları yeniden kurmak ile tamamen yeni matematik üretmek arasında net bir sınır olmadığını düşünüyorum
  • Matematik mantıksal olduğu için, bu tür aramalar için zaten çok sayıda algoritma vardır diye düşünüyorum; mesele basit bir arama problemi gibi görünmüyor
  • Ben de mevcut ispatların yeniden kurulması kısmına katılıyorum. LLM'in ürettiği sonucu doğrulamak hâlâ sıkıcı bir iş, ama yine de bunu insanın baştan yapmasından iyidir
    LLM'in asıl değeri, dil ile ifade edilebilen konularda yeni bakış açıları sunmasında yatıyor
  • Ben buna “bilimsel refactoring” diyorum. Örneğin, bir sabiti değiştirip mantığı yeniden çalıştırma türü deneyleri AI otomatikleştirebilir
  • Karmaşık teoremleri ispatlayabilen bir AI AGI değilse, o zaman AGI'nin ne olduğu gerçekten sorgulanır

• Problemi gerçekten çözen kişinin yazdığı açıklama yazısında, sonucun devasa bir pipeline olmadan, sadece birkaç prompt ile elde edilmiş olması etkileyici
  Son dönemdeki modeller çok daha fazla hesaplama kaynağı kullanıyor; bu yüzden bu sonuç daha çok alt sınır düzeyinde bir başarı gibi görünüyor

• Terence Tao, “AI contributions to Erdős problems” adlı bir wiki sayfası oluşturdu
  GitHub sayfasına ve Mathstodon gönderisine bakılırsa, bu sonuç (problem 728) o sayfadaki ilk 'yeşil madde', yani AI'ın gerçekten çözdüğü ilk örnek

  • İlginç biçimde, wiki'nin 6. bölümündeki AI ile biçimselleştirilmiş ispatların çoğu son birkaç ay içinde tamamlandı. Gelecek için heyecan verici

• Fizik ya da matematik gibi karmaşık alanlardaki uzmanların da AI ile konuşup yardım alıp almadığını merak ediyorum

  • Ben saf matematik doktorası sonrası veri bilimci olarak çalışıyorum. Literatür taraması ya da aşina olmadığım matematiği hızla gözden geçirme konusunda AI çok yardımcı oluyor
    Alanlara göre bakarsak fayda düzeyi programlama > uygulamalı ML > istatistik/uygulamalı matematik > saf matematik şeklinde azalıyor
  • Fizik uzmanı değilim ama AI sayesinde ihtiyaç duyduğum formülleri veya makaleleri bulmak için harcadığım zaman ciddi biçimde azaldı. Yine de sonuçları her zaman doğrulamak gerekiyor
  • Derin öğrenme modelleri ve yeni attention yapıları araştıran biri olarak ChatGPT, makale arama ve ilişkili fikirleri keşfetme konusunda çok faydalı
  • Matematikle hobi olarak ilgilenen biri olarak, LLM denemelerime geri bildirim veriyor ya da beni mevcut çözümlere yönlendiriyor. Eğlence olarak matematik için oldukça keyifli bir araç
  • Cebirsel geometri araştırıyorum; literatür araması dışında henüz büyük bir yardımını görmedim. Modeller arasında da ciddi fark var

• Aristotle'u şu anda doğrudan deneyebilirsiniz — https://aristotle.harmonic.fun/

  • AI'ı DeepMind'ın formal-conjectures veri kümesi ile test edip etmediklerini de merak ediyorum
  • Belgelerde “uvx aristotlelib@latest aristotle” yazıyor ama doğrusu aslında “uvx --from aristotlelib@latest aristotle”
    Ayrıca Stanford kişisel sayfası bağlantısı da hatalı (www kaldırılmalı)
  • Bu konu, ayrı bir HN başlığını hak edecek kadar ilginç. CEO olsam doğrudan bir tanıtım yazısı paylaşmayı düşünürdüm (referans bağlantı)

• Bu sonuç, tamsayılarla ilgili bir teorem üzerine ve Mathlib altyapısının güçlü biçimde desteklediği bir alana ait
  Kullanılan tanımlar da karmaşık değil; bu yüzden bu tür ispatların başarı şansı daha yüksek. Yine de gerçekten şaşırtıcı bir başarı

• Bu, LLM'lerin ötesine geçen uzmanlaşmış AI yaklaşımının potansiyelini gösteren bir örnek
  Aristotle makalesi arXiv:2510.01346 adresinde
  Transformer mimarisi kullanılıyor diye her şey LLM olmaz — dil verisiyle eğitilmediyse buna LLM denemez

  • Birçok kişi “LLM” ile “GenAI” terimlerini birbirinin yerine kullandığı için kafa karışıklığı doğuyor gibi görünüyor
  • “LLM olmayan yaklaşım” denmişti ama gerçekte ChatGPT kullanılmadı mı?
  • Evet, gerçekte ChatGPT kullanıldı
  • Makaleye bakılırsa, üç aşamanın tamamında da büyük transformer tabanlı LLM'ler rol alıyor
    1. Monte Carlo Graph Search içinde politika/değer fonksiyonlarını üstleniyor
    2. Gayriresmî akıl yürütme sistemi chain of thought kullanıyor
    3. AlphaGeometry de sinirsel-sembolik dil modeli kullanıyor
       Yani tüm aşamalar LLM tabanlı

• 2026'da AI'ın matematiğin çözülmemiş problemleri üzerinde giderek daha fazla çalışacağını düşünüyorum
  Bu örnek tamamen otonom değildi ama insan geri bildiriminin ardından AI neredeyse kendi başına çözmüş sayılır
  Artık “LLM'ler sadece olasılıksal papağanlardır” tartışmasının bittiğini düşünüyorum. Bundan sonra asıl mesele bunu nasıl pratikte kullanacağımız olacak

  • 2026'da matematik alanında patlayıcı ilerleme görebiliriz gibi geliyor
  • Bu sonuç büyük olasılıkla eğitim verisindeki benzer ispatların bir remiksi, ama bu remiks yeteneğinin kendisi zaten güçlü
  • Yine de bağımsız doğrulama şart. Sadece şirketin iddialarına dayanarak güvenmek zor