İnsan matematikçiler, karşı örnek bulmada yapay zekanın gerisinde kaldı

• ChatGPT ve Claude ailesi modelleri yalnızca birkaç hafta içinde Erdős'ün birim uzaklık varsayımı, Grothendieck'in grup şemaları sorusu ve Jacobian Conjecture için karşı örnekler üretti; bunların bazıları Lean ile doğrulandı
• OpenAI'nin Sol modeli, Erdős karşı örneğini ve bunun için gereken küresel sınıf cisimleri kuramı sonuçlarını 3 haftada 1,2 milyon satır Lean koduyla formelleştirdi; bu, 9 yılda yazılan 2,3 milyon satırlık mathlib'in yarısından fazlasına denk geliyor
• Grothendieck'in 60 yıllık sorusu için Sol 12 sayfalık bir karşı örnek buldu, Fable ise bunu 4 saat içinde 1.076 satırla formelleştirerek mertebesi 4 olan ama 4 tarafından yok edilmeyen bir grup şemasının varlığını doğruladı
• Otomatik formelleştirme araştırma hızını da büyük ölçüde artırdı; Andrew Yang yaklaşık 2 haftada 250 bin satır Lean kodu yazarak Fermat'nın son teoremi için gereken modülarite yükseltme teoremi projesini fiilen tamamladı
• Yapay zekanın ürettiği gayriresmî matematiğe olduğu gibi güvenilemez; ancak varsayımlar kesin Lean önermelerine dönüştürüldüğünde ispatlar ve çürütmeler mekanik olarak denetlenebilir, insanların ise karşı örneklerden daha derin matematiksel içgörüler çıkarması gerekir

---

Erdős'ün birim uzaklık varsayımı ve küresel sınıf cisimleri kuramı

• 20 Mayıs 2026'da ChatGPT, ayrık geometrinin Erdős birim uzaklık varsayımını çürüttü
  • 1960'larda Golod ve Shafarevich'in derin bir sayılar kuramı teoremini kullanarak bir karşı örnek kurdu
  • Birçok matematikçi argümanı önceden inceleyip geçerli olduğuna karar verdi, ancak yayımlandığı sırada Lean formelleştirmesi yoktu
• 26 Mayıs'ta Fields madalyalı ve Logical Intelligence baş bilim sorumlusu Mike Freedman, şirketinin sistemiyle ChatGPT makalesinin tamamını Lean'e otomatik olarak formelleştirdiklerini duyurdu
  • Formelleştirilen kapsam, Golod–Shafarevich teoreminin Erdős karşı örneğini gerektirdiği önermesiydi
  • Temeldeki sayılar kuramı teoreminin kendisi 100 sayfadan fazla gerektiriyor ve küresel sınıf cisimleri kuramının geniş bir kısmına dayanıyor
• 2025'teki Sınıf Cisimleri Kuramını Formelleştirme Yaz Okulu sonrasındaki bir yılda yerel durumlar neredeyse tamamlandı, ancak küresel durum çözümsüz kaldı

Sol'un ürettiği 1,2 milyon satırlık eksiksiz formelleştirme

• 26 Haziran'da OpenAI'den Boris Alexeev, yeni model Sol'u yönlendirerek Erdős karşı örneğinin, matematik aksiyomları dışında hiçbir şey varsaymayan eksiksiz bir formelleştirmesini yaptığını Lean Zulip'te açıkladı
• Sol, 3 hafta içinde 1,2 milyon satır Lean kodu üretti
  • 9 yılda yazılan mathlib 2,3 milyon satırdır
  • Kod kalitesi tutarlı değildi, ancak küresel sınıf cisimleri kuramının zor sonuçlarını ve sayı cisimlerinin kohomolojisine dair gayri-aşikar teoremleri gerçekten ispatladı
• Lean, keyfî komutlar çalıştırabilen bir programlama dili olduğu için, zararlı kod olasılığı göz önünde bulundurularak üretilen kod sandbox içinde çalıştırıldı
• Bu ölçek ve hız, büyük ölçekli yapay zeka üretimi matematik geliştirme sürecinin kaçınılmaz olduğu değerlendirmesine yol açtı

Formalizing Fermat atölyesi ve araç erişilebilirliği

• 6-10 Temmuz'da düzenlenen Formalizing Fermat atölyesine 25 kişi katıldı, ancak sponsor Logos Research'ün otomatik formelleştirme sistemini aynı anda yalnızca 5 kişi kullanabiliyordu
• Tüm katılımcılara bir aylık Claude Max aboneliği sağlanarak Claude Fable kullanmaları mümkün kılındı; OpenAI de bir aylık ChatGPT Pro erişimini ücretsiz verdi
  • Sol'un 9 Temmuz'da yayımlanması planlanıyordu
  • Fable'ın 7 Temmuz'da sona ermesi bekleniyordu, ancak fiilî erişim devam etti
  • Katılımcılar atölyenin 5 gününün 4'ünde Sol ve Fable'ı, tüm süre boyunca da Logos araçlarını kullanabildi
• Fermat'nın son teoreminin formelleştirilmesi için gereken sonlu düz grup şemaları kuramını geliştirmek amacıyla klasik makaleler Fable ve ChatGPT'ye verildi ve doğal dilde açıklamalar yazdırıldı
  • Logos, açıklamada yer alan bir önermenin yanlış olduğunu bulup açık bir karşı örnek sundu
  • Kontrol sonucunda, standart bir yapıyı tarif eden LLM üretimi belgenin hatalı olduğu ve insanların okurken hatayı kaçırdığı anlaşıldı
  • Sadece argümanı anlamadığını söylemek yerine argümanın yanlış olduğuna dair bir ispat sunması bakımından farklıydı

Grothendieck'in grup şemaları sorusu

• UChicago profesörü Akhil Mathew, her (n) mertebesindeki sonlu serbest grup şemasının (n) tarafından yok edilip edilmediğini soran Grothendieck'in eski sorusunu yapay zekaya önerdi
  • Deligne, değişmeli durum için ispat verdi
  • Grothendieck, taban uzayın reduced olduğu durum için ispat verdi
  • Rene Schoof daha fazla durumu ele aldı; Emiliano Torti de önceki yılki makalesinde daha genel bir durumu ispatladı
• Atölyeden sonraki gün, 11 Temmuz'da Sol bir karşı örnek bulup 12 sayfalık bir PDF üretti
  • Gayriresmî sonuç yerine tam Lean formelleştirmesi istenince Fable bunu 4 saat içinde 1.076 satırla otomatik olarak formelleştirdi
• Lean dosyasında dosya silme gibi komutlar olmadan yalnızca teoremlerin bulunduğu önce kontrol edildi, ardından dizüstü bilgisayarda derlendi
  • Önermede yalnızca mathlib kavramlarının kullanıldığı doğrulandı
  • Önermenin gerçekten bir karşı örneğin varlığını ifade edip etmediği denetlendi
  • İspatın düzgün biçimde derlenip derlenmediği kontrol edildi
  • Tüm doğrulama 5 dakikadan kısa sürdü
• Doğrulama sonucunda mertebesi 4 olan ama 4 tarafından yok edilmeyen bir grup şemasının var olduğu görüldü
• Akhil Mathew bu karşı örneği bir mathlib PR'ı olarak sundu
• Erdős karşı örneği yaklaşık 1 milyon satırken Grothendieck karşı örneği yaklaşık 1.000 satırla çok daha basitti; yine de 60 yıllık bir cebirsel geometri sorusunun makine tarafından çözüldüğü bir örnek oldu

Uzman tepkileri ve modülarite yükseltme teoremi

• 14 Temmuz'da Imperial College'dan bir profesör, Grothendieck karşı örneğinin kolayca bulunmasının yalnızca insanların bu problem üzerinde yeterince uzun düşünmediğini gösterdiğini değerlendirdi
• Doktora öğrencisi Andrew Yang, Fermat'nın son teoremi için önemli olan modülarite yükseltme teoremini Lean'de formelleştirirken Sol ve Fable'ı kullandı
  • Yaklaşık 2 haftada 250 bin satır Lean kodu yazdı
  • Bu sayede projeyi fiilen tamamladı
• Imperial'dan başka bir profesör, lisansüstü öğrencilerin Sol ve Fable'a ayda 200 dolar ödemesini anlamakta zorlanıyordu; ancak bu başarıyı gördükten sonra, doktora öğrencilerinin araca ayda 200 dolar harcamamasını daha çok irrasyonel buldu
• Harvard hâlihazırda tüm doktora öğrencilerine, doktora sonrası araştırmacılarına ve profesörlerine ücretsiz Fable erişimi sağlıyordu

Jacobian Conjecture karşı örneği

• Akhil Mathew ve Levent Alpöge, cebirsel geometride ek karşı örnekler bulma yollarını tartıştı; Fable yaklaşık 100 yıldır açık olan ünlü problem Jacobian Conjecture için bir karşı örnek buldu
• Levent Alpöge, 2026 Dünya Kupası finali sırasında çözülmüş gibi görünen sonucu X'te paylaştı
• Akhil Mathew yeni bir mathlib PR'ı önermeden önce, Paul Lezeau karşı örneği zaten elle formelleştirmiş ve DeepMind'ın Formal Conjectures deposuna PR göndermişti
• mathlib'de matematiksel varsayımların büyük ölçekli bir listesi yok, ancak Formal Conjectures deposu bunu barındırıyor
• İnsanlar bir varsayımın anlamını sadakatle yansıtan Lean önermesi üzerinde uzlaştığında, yapay zekanın ürettiği kodun o varsayımı ispatlayıp ispatlamadığını ya da çürütüp çürütmediğini kontrol etmek kolaylaşıyor

Biçimsel doğrulamadan sonra insanlara kalan görev

• Jacobian Conjecture'da bir sonraki adım, insanların söz konusu karşı örnekte tam olarak ne olup bittiğini anlama çalışmasıdır
• Grothendieck karşı örneği için de keyfî halka gösterimleri ve hesapları sıralama düzeyinin ötesine geçip daha derin bir anlayış geliştirmeye yönelik çalışmalar sürüyor
• Karşı örneklerin değeri, problemi biçimsel olarak kapatmakla sınırlı değildir; insanların matematiği daha iyi anlayabilmesi için içgörü çıkarma sürecinde tamamlanır

[GN⁺]

Hacker News yorumları

• Lisansüstü yıllarımda danışmanımın araştırma dersinde açık bir probleme doğrudan katkıda bulunma fırsatım olmuştu. Bir cuma günü hoca, doğru olmasını umduğu pürüzsüz ve güzel bir varsayım ortaya attı; ama tuhaf istisnaları seven ve ispat araçları da eksik olan ben, karşı örnek bulmaya odaklandım ve bir saat içinde buldum.
  Hoca tüm hafta sonu ispatlamaya çalışıp başaramadı; bu olay, aynı probleme farklı araçlara, beklentilere ve motivasyonlara sahip insanların baktığında bambaşka yönlerden katkı sunabileceğini gösteriyordu. Harika danışmanımla kıyaslanamazdım, ama o anda başka bir yöne bakmak için nedenim vardı ve bu da matematik araştırmasına yaptığım tek katkı olan küçük bir karşı örneğe yol açtı.

  • Makinelerin karşı örnek bulmakta iyi olmasının nedeni de burada yatıyor olabilir. Bir varsayıma yönelik estetik bir takıntıları yok ve çirkin sonuçlar ortaya koymaktan utanmıyorlar.
  • Bir matematikçi olarak benim hissim bunun tersi. İspatlar, bildiğiniz bir ispatı biraz değiştirerek yapılabilir; ama karşı örnek oluşturmak, nesnenin yapısını derinden anlamayı gerektirir ve bu çoğu zaman yeteneğimi aşar.
    Ancak bunun nedeni ağırlıklı olarak anlamakta zorlandığım soyut nesnelerle çalışmam olabilir; sayılar veya polinomlar söz konusu olduğunda bunun tersi büyük olasılıkla geçerlidir.
  • Henüz çözülememiş problemleri öğrencilere açan ve katılıma teşvik eden profesörler, araştırmacılar ve öğretmenler daha çok takdir edilmeli. Üniversitedeki ilk mühendislik dersimde eğitmen, birinci sınıflara “Bunlar henüz çözemediğimiz problemler; aklınıza bir fikir gelirse bize söyleyin” dediğinde, kendimi her zamankinden daha fazla hoş karşılanmış ve topluluğa dahil edilmiş hissetmiştim; kolayca sıkıcı olabilecek eğitimin başlangıcında büyük ilham vermişti.
  • 《How to Solve It》te de neredeyse aynı hikâye var.
  • Daha uç ve ters yönde bir Zeeman anekdotu var. Beş boyutlu uzayda düğümlenmiş bir küre bulmaya yıllarını harcadıktan sonra bunun imkânsız olduğunu fark etmiş ve birkaç saat içinde ispatlamış.
    https://ima.org.uk/28009/sir-erik-christopher-zeeman-the-mat...

• İkiz asal varsayımıyla ünlü Yitang Zhang, Purdue’da Tzuong-Tsieng Moh’un danışmanlığında Jacobian varsayımı üzerinde 7 yıl çalıştı. Doktora tezinin kilit adımının Moh’un hatalı bir sonucuna dayandığı ortaya çıktı; Moh tavsiye mektubu yazmayı reddetti ve Zhang eğitim ya da araştırma işi bulamayarak yıllarca Subway’de çalışmak zorunda kaldı.
  1986’da araştırmaya başladığında ChatGPT olsaydı nasıl olurdu merak ediyorum. Bugün dokunaklı bir başarı hikâyesine dönüştü, ama “Yu Xin’in hayatı baştan sona ıssızdı; yaşlılığındaki şiirleri ve fu’ları nehir geçitlerini sarstı” dizeleri gibi karmaşık duygular uyandırıyor.

  • Bir matematik doktora savunmasında jüri üyesinin ispatta bir kusur bulduğunu görmüştüm. Öğrenci bunu anladıktan sonra “Şimdi ne yapacağım?” diye sordu; jüri üyesi ise sadece omuz silkti.
  • Daha sonra ikiz asal varsayımındaki başarısı nedeniyle dokunaklı denebilir, ama akademide bu tür hikâyelerden bıktım. Siyaset ve itibar yönetimi fazlasıyla fazla; Zhang’ın böyle acılar yaşamaması gerekirdi.
    Araştırmamı matematiğe doğru genişletirken literatürdeki önermelerin önemli bir kısmının yanlış olduğunu ve uygulamalı literatüre kadar geniş biçimde yayıldığını görmek beni şaşırttı. Sorunu bildirseniz bile Zhang anekdotundaki gibi çoğu zaman savunma ve inkârla karşılaşıyorsunuz. LLM’ler ispatta yararlı, ama çok büyük hatalar da yapabiliyor; farklı sezgileriyle keşif yönü öneren bir başka kişi gibiler, bu yüzden 1986’da da sonuç muhtemelen aynı olurdu.
  • ChatGPT’nin aktardığı dizenin anlamı kabaca şu: “Yu Xin’in hayatı bütünüyle hüzünlüydü; yaşlılığındaki şiirleri ve fu’ları Jiangguan’ı sarstı.”

• Matematikte karşı örnekler, tanımları inceltmek ve ispatları keskinleştirmek açısından çok önemlidir. Imre Lakatos’un 1976 tarihli 《Proofs and Refutations》 kitabını öneririm; topoloji, olasılık kuramı, analiz gibi alanlarda yalnızca karşı örnekleri ele alan epey çok kitap da var.
  https://en.wikipedia.org/wiki/Proofs_and_Refutations
  https://www.amazon.com/s?k=counterexamples

• Karşı örnek bulmak, yanlış bir önermeyi ispatlamaya zaman harcamadan başka problemlere geçmeyi sağladığı için, en azından matematikte insanlığın zamanını daha üretken kullanmasını sağlar.

  • Karşı örnekle çürütme etkilidir, ama nihayetinde tatmin edici değildir. Cevap verir, fakat matematiğin neden öyle işlediğini anlamanızı sağlamaz ya da yeni sorulara götürmez.
    Neyin zarif ve içgörü dolu bir ispat olduğuna insanlar karar verdiği sürece insan matematikçilere iş kalacaktır.
  • Karşı örnekler, teoremin ifadesini düzeltmek için de yararlıdır. Kuramsal bilgisayar bilimi araştırmalarında, doğru olmasını umduğunuz bir teoremi ispatlamaya çalışırken karşı örnek bulmak, ifadeyi değiştirip devam etmek yaygındır.
    Bilgisayar bilimindeki birçok teoremin indüktif ve koindüktif tanımlarla uğraşması da yardımcı olur.
  • Özellikle karşı örnek biçimsel olarak doğrulanmışsa, yıllar süren varsayımsal çabayı neredeyse anında kesin bir cevaba dönüştürür.
  • Ama genel olarak zamanın daha üretken kullanıldığını kesin söyleyemeyiz. Bir önermeyi ister ispatlayın ister çürütün, sonunda doğru ya da yanlış olsun, süreç içinde yeni içgörüler doğabilir.

• Matematik versiyonu 《John Henry Baladı》nı da muhtemelen yapay zeka yazacak. Makinelerin bile aşamayacağı, “THE BOOK’a girecek türden” bir ispat ortaya koyacak son insan şampiyonun kim olacağını merak ediyorum.
  https://en.wikipedia.org/wiki/John_Henry_(folklore)
  https://en.wikipedia.org/wiki/Proofs_from_THE_BOOK

  • Bu, matematiği futbol taraftarı gibi rekabet olarak gören sağlıksız bir bakış açısı. Matematikte en değerli şey yalnızca güzel ispatlar değil, yararlı tanımlardır; iyi tanımlar ve onlardan iyi varsayımlar üretmek, LLM’lerin henüz fethetmeye çalışmadığı bir alan.
  • Henüz o kadar dramatik değil, ama yakında o aşamaya gelmesi mümkün. Yapay zeka yeteneklerinin asimptotik olarak mı gelişeceğini yoksa hızlanacağını mı yapısal olarak öngörebileceğimiz bir dayanak yok; hangi problemin yeni yöntemlerle çözüleceği konusunda da iki olasılık da açık.
    Yapay zeka yeteneklerinin iç işleyişini ve büyüme eğrisini anlamıyoruz; performansı kasıtlı olarak düşük gösterip göstermediklerini bile tam olarak bilemeyiz. Ölçüme direnen belirimsel bir olgu da olabilir, birkaç yıl sonra saat gibi öngörülebilir hale de gelebilir. Kimse bilmiyor; bilen varsa söylemiyor ve sesi en çok çıkanların da bildiği bir şey yok.

• Bir lisansüstü öğrencinin anlamlı sonuçlara ulaşmasını ciddi ölçüde hızlandırıyorsa, öğrenci başına yılda 2.400 dolar yatırım yapmamak için bir neden yok. Toplam maliyet içinde neredeyse bozuk para sayılır

  • Bazı lisansüstü öğrenciler kendilerini “anlamlı sonuçlar üreten bir makine” değil, etik bir varlık olarak görüyor. Yararlı LLM’lerin bile çalınmış eğitim verileri ve devasa çevresel etkileri nedeniyle meşrulaştırılmasının zor olduğunu herkes biliyor
  • EPSRC doktora programı geçim bursu yaklaşık 20.000 £ olduğundan, yıllık maliyetin yaklaşık %10’una denk geliyor. Öğrencinin kendisi için büyük bir yük

• Üniversite yıllarında LLM’in ürettiği Lean biçimselleştirmeleri olsaydı iyi olurdu. Ders slaytlarındaki matematikte çok hata vardı; bazı profesörler “kanıt slaytta var” diyerek açıklama taleplerini reddederken hataları kabul etme konusunda da isteksizdi
  Lean kanıtlarının kendisi çoğu zaman anlamaya uygun değil, ama bunlara dayanarak insanların daha kolay anlayacağı argümanlar üretilebilmesini umuyorum

  • İlk iddiaya katılmak zor. Öğrenme eğrisi dik olsa da iyi yazılmış Lean·Agda·Rocq biçimselleştirmeleri kanıtı anlamak için mükemmeldir. İyi bir biçimselleştirme, genel çerçeveyi ve temel argümanı yapısal biçimde gösterir; kâğıt üzerindeki kanıttan farklı olarak her adımın ayrıntılarını istediğiniz derinliğe kadar kontrol etmenizi sağlar
    Martín Escardó’nun TypeTopology Agda deposu buna iyi bir örnek. Buna karşılık, mevcut LLM’lerin ürettiği biçimselleştirmeler çok dağınık olabiliyor; doğruyu sertifikalandırsa ve ilginç bir argüman içerse bile, matematiksel anlayışı artıracak bir forma getirmek ciddi çalışma gerektiriyor. Etkileşimli Agda öğreticisi lets-play-agda.quasicoherent.io adresinde
  • Biçimselleştirme, tartışmayı bitiren ve şüpheyi tamamen ortadan kaldıran Leibnizci yaklaşım için de kullanılabilir

• Matematikçiler için karşı örneklerin, fizik bilimlerindeki beklenmedik sonuçlar gibi o anda can sıkıcı olsa da modelin yanlışlığını ortaya koyduğu için son derece önemli şeyler mi, yoksa programlamadaki hata raporları gibi küçük ve uğraştırıcı ayrıntılar mı olduğunu merak ediyorum

  • Karşı örnekler koşulların rolünü netleştirir. Bir kanıttaki her koşul ihlal edildiğinde neyin başarısız olduğunu gösteren, mümkün olan en basit ve akılda kalıcı karşı örnekler varsa bu çok yararlıdır
    Matematikçiler kafalarında bir karşı örnek hayvanat bahçesi taşımaya eğilimlidir. Bir teoremi yeniden kurarken de keskin ve akılda kalan karşı örnekleri düşünerek, onları dışarıda bırakacak şekilde tanım kümesini ve koşulları daraltabilirler
  • 《Counterexamples in Topology》 ve 《Counterexamples in Analysis》 gibi, alanın inceliklerini karşı örnekler üzerinden öğreten eğitim kitapları var. Yalnızca hedeflenen normal nesneleri öğrenmektense patolojik ve dejenere örnekler üzerinden ayrıntıları kavramak daha kolay olduğu için popülerler

• Bu matematiğin önemli bir kısmını anlamak zor, ama genel olarak teorem kanıtlarıyla ilgili görünüyor. Yapay zekâ matematiği hızlanmaya devam ederse, ileride mühendislikte veya biyomedikalde uygulanacak yeni matematiği de keşfedip keşfetmeyeceğini; insanlığın büyük bir atılımın hemen eşiğinde mi olduğunu, yoksa yalnızca zaten bilinen şeyleri kanıtlamakla mı sınırlı kalacağını merak ediyorum

  • Olası. Sıkıştırılmış algılama, biyomedikalde uygulanan yeni matematiğe bir örnek olarak görülebilir; MRI çekim sürelerini ciddi biçimde azaltarak hasta deneyimini iyileştirebilir ve daha fazla hastanın tetkik yaptırmasını sağlayabilir
    https://en.wikipedia.org/wiki/Compressed_sensing
  • Mühendislik ve biyomedikalde uygulanması muhtemelen uzun vadeli bir mesele olur, ama yeni matematiksel yöntemlerin gelişimi temel fizik araştırmaları için daha erken aşamada önem kazanabilir. Evren modellerinin ifade edilmesini veya doğrulanmasını mümkün kılan matematik araçları ortaya çıktığında, modellerin büyük ölçüde iyileştiği sıkça görüldü
  • Mümkün olsa bile çok uzun zaman alacaktır. Çoğu uygulama alanında, yüzlerce yıl önceki matematik bile ancak şimdi doğru dürüst kullanılmaya başlanıyor

• Bir gün matematikçiler incelemeleri gereken kanıtların altında kalabilir ve aşırı güvenilen yanlış önermeler matematik dünyasına girebilir. Geleceğin matematikçileri, yapay zekâ kullanan yazılım mühendisleri gibi yapay zekâ tarafından üretilmiş binlerce satır kanıtı inceleyip ince hataları aramak zorunda kalabilir

  • O nokta aslında çoktan geçildi. Günümüz literatürü çok geniş ve hatalı kanıtlarla dolu; yayımlanmış sonuçlar arasında da sayısını bilmesek bile kesinlikle sıfır olmayan miktarda yanlış sonuç bulunuyor