Erdős Problem web sitesinde yapay zeka desteği sıradanlaşıyor

• Erdős Problem #367 çözüm sürecinde yapay zeka araçlarının kilit rol oynadığı ve insan matematikçilerle iş birliği yaptığı bir örnek rapor edildi
• Wouter van Doorn, problemin ikinci kısmı için insan tarafından üretilmiş bir karşı örnek sundu; ardından Gemini Deepthink ilgili kongruansın tam ispatını oluşturdu
• Terence Tao, Gemini’nin p-adik cebirsel sayı teorisine dayalı ispatını daha basit bir biçime dönüştürerek paylaştı ve ardından Lean ile biçimselleştirme olasılığından söz etti
• Boris Alexeev, Harmonic’in Aristotle aracı ile Lean biçimselleştirmesini tamamladı; yapay zeka kötüye kullanımını önlemek için nihai önerme manuel olarak doğrulandı
• Bu süreçler dizisi, matematik araştırmalarında yapay zeka desteğinin giderek standart bir prosedür haline geldiğini gösteriyor

---

Erdős Problem #367 için yapay zeka iş birliği örneği

• 20 Kasım’da Wouter van Doorn, problemin ikinci kısmı için bir karşı örnek sundu; bu, belirli bir kongruansın doğru olduğu varsayımına dayanıyordu
  • İlgili kongruansın geçerliliğinin başka katılımcılar tarafından doğrulanmasını istedi
• Birkaç saat sonra Terence Tao, bu problemi Gemini Deepthink’e sundu ve yaklaşık 10 dakika içinde kongruansın tam ispatını ve tüm argümanın doğrulamasını aldı
  • Gemini’nin ispatı p-adik cebirsel sayı teorisi kullanıyordu; Tao ise bunu daha basit, daha temel bir ispat biçimine dönüştürerek sitede paylaştı
  • Tao, bu ispatın Lean’da ‘vibe formalizing’ için uygun olabileceğini belirtti

Lean biçimselleştirmesi ve doğrulama

• İki gün sonra Boris Alexeev, Harmonic’in Aristotle aracını kullanarak Lean biçimselleştirmesini tamamladı
  • Yapay zeka kötüye kullanımını önlemek için nihai önerme doğrudan manuel olarak biçimselleştirildi
  • Tüm süreç yaklaşık 2~3 saat sürdü ve ortaya çıkan çıktı çevrimiçi olarak paylaşıldı
• Tao daha sonra yapay zeka kullanarak literatür taraması yaptı; ilişkili bazı çalışmalar bulunsa da #367 ile doğrudan ilgili bir şey bulunamadı

Topluluk tepkisi ve tartışma

• Bazı kullanıcılar, Tao’nun güncellemesi üzerinden yapay zekanın akademik matematikteki kullanım durumunu ilgiyle takip ediyor
• Diğer kullanıcılar, Lean’ın biçimselci yaklaşımına eleştirel yaklaşıyor ve matematiksel anlayışın bir sıkıştırma (compression) olduğunu, Lean’ın ise bunu düşük seviyeli ayrıntılara açtığını (decompression) söylüyor
  • İlgili “Against Lean: Why Proof Assistants Formalize the Wrong Thing” belgesi, Lean benzeri ispat yardımcılarının matematiğin özünü yanlış yakaladığını savunuyor
• Başka bir kullanıcı ise yapay zeka sohbetlerinin doğruluk sorunlarına değinerek, ince ayar gerektirse de kullanmasının keyifli olduğunu değerlendiriyor

[GN⁺]

Hacker News görüşleri

• Matematik ağırlıklı ML makalelerini bir yapay zeka asistanına verip basit açıklamalar ya da sözde kod olarak geri alabilmek şaşırtıcı bir deneyim
  Üniversitede öğrendiklerimi 25 yılı aşkın süredir hiç kullanmamış biri olarak bu gerçekten büyük yardım

  • Bu açıklamanın doğru olup olmadığını nasıl doğruladığını merak ediyorum. Matematiksel tanımlarda çok ince nüanslar var
  • Bence LLM'lerin öğrenmede parladığı alan tam da burası
    Makaleyi Claude'a verip bir özet aldıktan sonra sorular sormaya devam edebiliyorsun
    Lisans ya da yüksek lisansta öğrenmediğim biyoloji gibi alanlarda bile, bilgili bir özel ders hocasıyla konuşur gibi derine inebildim
  • Matematik gösterimi bağlama çok bağımlı, bu yüzden LLM'den bunu Lisp gibi bağlamı düşük bir dile çevirmesini istemek yapıyı çok daha hızlı kavramayı sağlayabiliyor

• Araştırmacıların ve şirketlerin bilimsel araştırmada daha fazla verimlilik artışı elde etmesini umuyorum
  Kusursuz olmayan bir asistan bile kaldıraç etkisini ciddi biçimde artırıyor

  • Tao'nun bahsettiği iOS için formalleştirme uygulaması beta sürümünde var → Aristotle
    Robinhood CEO'sunun kurduğu bir startup olduğu söyleniyor

• 'Vibe formalizing', 'vibe engineering' ve 'vibe coding'in mantıksal uzantısı gibi geliyor
  Problemin parçaları tam oturmadığında, gayriresmî yöntemlerle matematiksel titizliği birleştiren 'Move 37 as a Service' benzeri bir yaklaşım ilginç

  • Daha önce polyhedral compilation üzerine bir makale okurken takıldığım bir nokta olmuştu; ChatGPT akıl yürütme sürecini iyi yönlendirmişti
    Elbette yanlış kısımlar da vardı ama benim kafa karışıklığımı yansıtan bir diyalogla anlayışımı derinleştirebildim
    Yapay zeka, kullanıcının kafasının karıştığı noktaları saptamada özellikle güçlü

• Macar matematikçi Erdős'ün adının telaffuzuyla ilgili bir şey duydum
  Macarcada yazım ve telaffuz neredeyse tamamen örtüşür ama isimlerde istisnalar var
  İngilizceye yakın biçimde kabaca “airdish” gibi duyulduğu söyleniyor

  • Ő aslında sadece œ(oe) sesidir. Macar soyadlarındaki -y, soylu kökeni ifade eden -i ekinin bir kalıntısıdır
    Örnek: Görgey, Széchényi, Lánczos
    Macar isim sırası da Japoncadaki gibi soyadı-ad(big endian) düzenindedir. Örnek: “Erdős Pál”, “Neumann János”
  • 1960'ta matematik bölümü panosunda gördüğüm mizahi bir şiir vardı — Erdos'un yazdığı bir makalenin 'çemberler yuvarlaktır' teoremini çürüttüğü şakası yapılıyordu
  • Diller arasında telaffuz işaretlerinin (aksanların) anlamı değiştiği için, Macarca işaretleri İngilizce bir cümlede doğrudan kullanmak bana tuhaf geliyor
  • Başta “airdish” telaffuzu garip gelmişti ama 'os' sonunu damaksıllaştırınca (palatalize edince) kulağa mantıklı gelmeye başladı
  • Amerikalı olmadığım için olabilir ama kimsenin bu tür telaffuz meselelerini umursamadığı hissine kapılıyorum

• Yorumlarda anti-Lean eğilimli tepkiler olması ilginç

  • Matematikçi değilim ama Lean karşıtı o materyalin güvenilir olup olmadığını merak ediyorum
    Sadece farklı bir yaklaşımı mı pazarlıyorlar, yoksa felsefi olarak mı Lean'a karşılar, öğrenmek isterim
  • Tao gibi ünlü isimler doğal olarak tuhaf tiplerin ve komplo teorisyenlerinin ilgisini çok çeker

• Araştırma matematiğinde yapay zeka kullanma deneyimim karışık oldu
  Önemsiz olmayan bazı argümanları otomatik tamamlasa da bazı alanlarda tamamen yolunu kaybediyor
  Şimdilik yapay zekanın matematikçilerin yerini almasından çok yardımcı araç olarak faydalı olduğu bir aşamadayız diye düşünüyorum

  • Benim de benzer bir deneyimim oldu. Bir makaledeki basit bir permütasyon hesaplama problemini çözmesini istedim ama kendim çözmemden daha uzun sürdü
    Kodlamada da ufak tefek bug'ları yakalayamadığı oldu ama karmaşık işlerde büyük yardım sağladı
    Sonuçta bu araçlar uzmanların yerini almaktan hâlâ çok uzak ve abartılı pazarlama güveni zedeleyebilir
    Hani derler ya, 'ayı vaat ettiysen ayı vermelisin'; gerçekçi beklentiler önemli

• Hayatımda bir gün 'Star Trek'teki gibi “Bilgisayar, bana bu matematik probleminin ispatını çiz” diyebileceğimiz bir çağın geleceğine inanmazdım
  “Beam me up Scotty” de mümkün olsaydı keşke

  • Ama o durumda her seferinde ölebileceğimiz için, o kısmı biraz sorunlu olurdu

• Bu gece araba kullanırken ChatGPT ile LLVM ve GCC pipeline scheduler ayrıntıları üzerine konuştum
  Bu sayede verimliliğim ciddi biçimde arttı ve üzerinde deneme yaptığım derleyici notlarını otomatik olarak düzenledi
  Eskiden hayal bile edilemeyecek bir şeydi bu

  • Benim deneyimime göre LLM'in bazı ayrıntılarda hata yapmış olma ihtimali yüksek
    Elbette sonuçlar kişiden kişiye değişebilir

• Yapay zekanın adını Erdos koyarsak sanırım hepimizin Erdos numarası 1 olur

  • Ya da DR-DOS'un devamı gibi geliyor
  • Gerçekten de AI entegre IDE olan Erdos adlı bir ürün var

• Mevcut frontier araçlarını iyi kullanarak işbirlikçi bir matematik araştırma ortamı kurabilmiş olması etkileyici

  • Neyse ki matematik, putlaştırmanın ya da popülerlik yarışının sonuçların doğruluğunu belirlemediği bir alan
    Bu yüzden matematiğin hâlâ sahte bilimsel etkilerden görece bağımsız kalan ender disiplinlerden biri olduğunu düşünüyorum