Yapay zeka dünyası, 1 Ağustos 2026'da OpenAI'nin yaptığı bir duyuruyla sarsıldı: Şirketin henüz kamuya açıklanmamış yeni nesil model ailesi "Astra", matematik ve teorik bilgisayar bilimi alanında onlarca yıldır çözülemeyen on açık problemi çözdüğünü ve bu sonuçları makine tarafından doğrulanabilir kanıtlarla birlikte yayımladığını duyurdu. İddia büyük, ama bu kez arkasında daha sağlam bir doğrulama süreci var. Bu yazıda Astra'nın ne yaptığını, hangi problemleri çözdüğünü, maliyetini, matematik camiasının tepkisini ve bir önceki benzer iddianın neden çöktüğünü ayrıntılı şekilde ele alıyoruz.
Astra modeli ne zaman ve nasıl duyuruldu?
OpenAI, 1 Ağustos 2026'da resmi blogunda "Ten advances in mathematics and theoretical computer science" başlıklı bir yayın paylaştı. Duyuruya göre, henüz piyasaya sürülmemiş olan Astra modelinin dahili bir versiyonu, matematik ve teorik bilgisayar biliminde uzun süredir çözülemeyen on probleme çözüm üretti. Sonuçlar, 249 sayfalık bir makale koleksiyonu halinde toplandı ve her biri için GitHub üzerinde Lean 4 formatında makine tarafından doğrulanabilir sertifikalar yayımlandı.
Sürecin işleyişi de dikkat çekici: Model önce çözümleri üretti, ardından insan araştırmacılar bu argümanları akademik makale formatına dönüştürdü, son olarak model kendi kanıtlarını Lean sertifikalarına dönüştürdü. OpenAI ayrıca her sonuç için modelin "düşünce sürecinin" (chain-of-thought) bir anlatımını da paylaştı. OpenAI'nin matematik araştırmalarından sorumlu ismi Sebastien Bubeck sonuçları "güzel" olarak nitelendirirken, araştırmacı Noam Brown bunu "bilimsel akıl yürütme için büyük bir adım" olarak tanımladı.
Çözülen 10 matematik problemi nedir?
Sonuçlar tek bir alana değil, grup teorisi, yüksek boyutlu geometri, kodlama teorisi, kuantum karmaşıklığı, kafes kriptografisi ve ekstremal kombinatorik olmak üzere altı farklı matematik dalına yayılıyor.
| Alan | Öne çıkan sonuç |
|---|---|
| Grup Teorisi | İlk açık non-sofic grup inşası (1999'dan beri açık) |
| Operatör Cebirleri | Connes'in sertlik varsayımının çürütülmesi |
| Geometri | Ehrhart'ın hacim varsayımının kanıtı |
| Yüksek Boyutlu Geometri | 1978'den beri ilk küre paketleme üst sınırı iyileştirmesi |
| Kodlama Teorisi | İkili ve küresel kodlarda üstel sınır iyileştirmesi |
| Ekstremal Kombinatorik | 3 Erdős problemi (183 dahil, Ramsey sayıları) |
Non-sofic grup inşası: 27 yıllık bilmecenin çözümü
Duyurunun başlık sonucu, ilk açık "non-sofic grup" inşasıydı. Matematikçi Mikhail Gromov'un 1999'da ortaya attığı "soficity" kavramından bu yana, her grubun sonlu permütasyon sistemleriyle yaklaşık olarak temsil edilip edilemeyeceği (yani "sofic" olup olmadığı) açık bir soruydu. Günlük matematikte kullanılan hemen hemen tüm gruplar (amenable ve residually finite gruplar dahil) bu koşulu sağlıyordu. Astra'nın ürettiği açık inşa, bu koşulu sağlamayan en az bir grubun var olduğunu somut biçimde gösterdi. Bu sonucun etkileri operatör cebirleri teorisi, ergodik teori ve hücresel otomatlar çalışmalarına kadar uzanıyor.
Connes'in sertlik varsayımının çürütülmesi
Astra ayrıca, aynı von Neumann cebirini paylaşan sonsuz sayıda izomorf olmayan (T) özelliğine sahip grup inşa ederek Connes'in sertlik varsayımını çürüttü. Bunun yanında Ehrhart'ın hacim varsayımını da kanıtladı.
Küre paketleme, kodlama teorisi ve diğer sonuçlar
Sonuçlar arasında, 1978'den bu yana ilk kez yüksek boyutlu küre paketleme yoğunluğunda Cohn–Elkies eşiğine kadar inen yeni üst sınırlar da yer alıyor. Ayrıca, belirli bir minimum mesafedeki ikili kodların ve yüksek boyutlu küresel kodların maksimum boyutuna ilişkin üstel olarak iyileştirilmiş sınırlar üretildi.
Üç Erdős problemi
Listede, matematikçi Paul Erdős'ün ünlü açık problemler kataloğundan üç problem de bulunuyor; bunlardan biri çok renkli Ramsey sayılarına ilişkin 183 numaralı problemdi.
"Belki birim mesafe kanıtı kadar büyük olmayabilir ama inşalar açısından bu büyük bir gelişme." — Thomas Bloom, erdosproblems.com kurucusu
Kanıtlar nasıl doğrulandı? Lean 4 ve insan-yapay zeka işbirliği
Burada kritik nokta, kanıtların soyut iddialar değil, Lean 4 kanıt asistanıyla biçimsel olarak doğrulanmış sertifikalar şeklinde sunulmuş olması. Lean'in derleyicisi, bir kanıttaki mantıksal adımların birbirinden doğru şekilde çıktığını garanti ediyor; yani bir adım mantıksal olarak tutarsızsa derleyici bunu kabul etmiyor. Ancak bunun bir sınırı var: Lean, problemin matematikçilerin kastettiği anlamda doğru "biçimlendirildiğini" bağımsız olarak teyit etmiyor — bu kontrolü hâlâ insan uzmanlar yapmak zorunda. Sonuçlar henüz hakemli bir dergide resmi olarak yayımlanmadı; şu ana kadar yalnızca ön baskıları gören matematikçiler tarafından gayriresmi şekilde incelendi.
Lean 4 doğrulaması, bir kanıtın mantıksal olarak tutarlı olduğunu garanti eder; ancak problemin matematikçilerin kastettiği anlamda doğru kurulduğunu (formalize edildiğini) garanti etmez. Bu ayrım, sonuçların tam bilimsel kabulü için hâlâ önemli.
Maliyet: Neden sadece 2.000 dolar?
OpenAI, on çözümün üretilmesi için harcanan toplam token maliyetinin, mevcut API fiyatlandırmasıyla yaklaşık 2.000 dolar olduğunu açıkladı. Bu rakamın modelin yolda başarısız olduğu diğer denemeleri kapsamadığını, yalnızca yayımlanan başarılı sonuçların maliyetini yansıttığını belirtmekte fayda var. Yine de, insan matematikçilerin yıllarca üzerinde çalıştığı problemlerin bu ölçekte düşük bir maliyetle üretilmiş olması, araştırma ekonomisi açısından dikkat çekici bir emsal oluşturuyor.
Artıları ve eksileri
- Artı: Sonuçlar altı farklı matematik alanına yayılıyor, tek bir dar kategoriye sıkışmıyor.
- Artı: Her kanıt, herkesin bağımsız olarak doğrulayabileceği makine tarafından kontrol edilebilir Lean sertifikalarıyla destekleniyor.
- Artı: Süreç şeffaf: modelin düşünce süreci de yayımlandı.
- Eksi: Sonuçlar henüz hakemli dergilerde resmi olarak yayımlanmadı; peer-review süreci zaman alacak.
- Eksi: Astra modelinin kendisi hâlâ kamuya açık değil; iddialar OpenAI'nin kendi açıklamalarına dayanıyor.
- Eksi: Bir önceki benzer iddianın (Ekim 2025) çürütülmüş olması, camiada temkinli bir yaklaşımı gerekli kılıyor.
Kullanım alanları: Bu neden önemli?
Bu gelişme sadece matematikçiler için değil, yapay zekanın "orijinal" ve doğrulanabilir bilimsel katkı üretip üretemeyeceği sorusuna verilen yanıt açısından da önemli. Eğer bu yaklaşım güvenilir şekilde ölçeklenirse, ilaç keşfinden malzeme bilimine, kriptografiden yazılım doğrulamasına kadar, insan uzmanların yıllar sürdürdüğü biçimsel doğrulama gerektiren araştırma süreçlerinde yapay zekanın araştırma asistanı ötesinde bir rol üstlenmesi gündeme gelebilir. Lean gibi biçimsel doğrulama sistemleriyle birleşen bir yapay zeka modelinin, "halüsinasyon" riskini en aza indirerek güvenilir sonuçlar üretebileceği fikri, bilim camiasında hem heyecan hem tartışma yaratıyor.
Rakipler ve sektördeki konum
OpenAI bu alanda tek oyuncu değil. Google DeepMind, matematik yarışma problemlerinde güçlü sonuçlar üreten modelleriyle biliniyor; Anthropic ve DeepSeek gibi şirketler de akıl yürütme (reasoning) odaklı modellerini geliştirmeye devam ediyor. Ancak Astra'nın öne çıkan farkı, sonuçların açık matematik literatüründe daha önce çözülmemiş, gerçek anlamda özgün problemlere odaklanması ve bunun biçimsel kanıtlarla desteklenmesi. Bu, rekabeti "kim daha hızlı yanıt üretiyor" sorusundan "kim doğrulanabilir bilimsel katkı üretiyor" sorusuna doğru kaydırıyor.
Geçmiş tartışma: Ekim 2025'teki Erdős iddiası neden çöktü?
Bu haberin güvenilirliğini değerlendirirken geçmişe bakmakta fayda var. Ekim 2025'te, dönemin OpenAI yöneticilerinden Kevin Weil, GPT-5'in on Erdős problemini çözdüğünü iddia etmişti. Ancak bu iddia günler içinde çöktü: erdosproblems.com'u yöneten matematikçi Thomas Bloom, modelin aslında orijinal kanıtlar üretmediğini, literatürde zaten var olan çözümleri bulup getirdiğini gösterdi. Astra duyurusu bu açıdan yapısal olarak farklılaşıyor: sonuçlar tek bir katalogdan değil altı ayrı matematik alanından geliyor, kanıtlar Lean 4 ile herkesin doğrulayabileceği şekilde biçimselleştirilmiş ve bizzat geçen seferki iddiayı çürüten Bloom, bu sonucu "büyük haber" olarak nitelendirdi; hatta Mayıs 2026'da aynı model ailesinin çürüttüğü Erdős birim mesafe varsayımından bile daha önemli bulduğunu belirtti.
Matematik camiasının tepkisi ve Leiden Deklarasyonu
Bu gelişme, yapay zeka şirketleriyle matematik camiası arasındaki gerilimin arttığı bir dönemde geldi. Haziran 2026'da, Uluslararası Matematik Birliği'nin de desteklediği "Leiden Deklarasyonu" imzalandı; bu deklarasyon, yapay zeka şirketlerinin yayımlanmış araştırmaları izin almadan kullandığını, hakemli değerlendirme süreçlerini atladığını ve kanıt ile atıf bütünlüğünü tehdit ettiğini vurguluyordu. Deklarasyon özellikle sonuçlarını hakemli dergiler yerine basın bültenleriyle duyuran şirketleri hedef almıştı. Bu bağlamda, Astra sonuçlarının bilim camiası tarafından tam olarak "kabul edilmesi", biçimsel doğrulamanın ötesinde, alanın yavaş işleyen hakemli değerlendirme ve tekrar üretilebilirlik sürecini de gerektirecek.
Astra'nın geleceği: Sıradaki büyük model mi?
Astra, OpenAI'nin "bir sonraki büyük model ailesi" olarak tanımlanıyor ve bu duyuru aynı zamanda modele resmen bir isim kazandırdı. Bazı haberlerde, modelin çoklu ajanların karmaşık problemler üzerinde saatlerce, hatta günlerce birlikte çalışabilmesini sağlayacak bir mimariye sahip olduğu belirtiliyor. Ancak modelin resmi çıkış tarihi, tam teknik özellikleri ve "GPT-6" olup olmayacağı henüz OpenAI tarafından doğrulanmadı; bu noktalar şu an için spekülasyon düzeyinde kalıyor.
Sonuç
OpenAI'nin Astra modeliyle duyurduğu on matematik sonucu, yapay zekanın bilimsel araştırmadaki rolü konusunda önemli bir kilometre taşı olabilir — ama henüz tamamlanmamış bir hikayenin ilk bölümü. Lean 4 sertifikaları sayesinde mantıksal tutarlılık güçlü şekilde doğrulanmış olsa da, sonuçların hakemli dergilerde resmi olarak kabul görmesi, alanın onu gerçekten "özümsemesi" zaman alacak. Geçmişteki başarısız iddianın izlerini taşıyan bir camiada, temkinli iyimserlik şu an için en makul yaklaşım gibi görünüyor.
Sık sorulan sorular
OpenAI Astra nedir?
Astra, OpenAI'nin henüz kamuya açıklanmamış bir sonraki büyük model ailesinin adıdır. 1 Ağustos 2026'da yapılan duyuruyla, modelin dahili bir versiyonunun on açık matematik problemini çözdüğü belirtildi.
Astra hangi problemleri çözdü?
Grup teorisi, yüksek boyutlu geometri, kodlama teorisi, kuantum karmaşıklığı, kafes kriptografisi ve ekstremal kombinatorik alanlarında toplam on problem çözüldü; bunlar arasında ilk non-sofic grup inşası, Connes'in sertlik varsayımının çürütülmesi ve üç Erdős problemi yer alıyor.
Astra'nın sonuçları güvenilir mi, yoksa Ekim 2025'teki gibi çürütülür mü?
Şu ana kadarki tepkiler olumlu yönde; geçen seferki iddiayı çürüten matematikçi Thomas Bloom bile bu sonucu "büyük haber" olarak nitelendirdi. Ancak sonuçlar henüz hakemli dergilerde resmi olarak yayımlanmadı, bu nedenle tam bilimsel kabul süreci devam ediyor.
Lean 4 kanıt sertifikası ne işe yarar?
Lean 4, bir matematiksel kanıttaki her adımın mantıksal olarak doğru şekilde birbirinden çıktığını otomatik olarak kontrol eden bir yazılımdır. Bu, kanıtın iç tutarlılığını garanti eder ama problemin doğru formüle edildiğini garanti etmez; bunu hâlâ insan uzmanlar kontrol etmelidir.
Astra sonuçlarının maliyeti neden bu kadar düşük?
OpenAI, on çözümün üretilmesi için harcanan toplam hesaplama maliyetinin yaklaşık 2.000 dolar olduğunu açıkladı. Bu rakam yalnızca başarılı sonuçların maliyetini kapsıyor, modelin başarısız olduğu diğer denemeleri içermiyor.
Astra, GPT-6 mı olacak?
Bu konu henüz OpenAI tarafından resmi olarak doğrulanmadı. Astra, şirketin "bir sonraki büyük model ailesi" olarak tanımlanıyor ancak kesin isimlendirme ve çıkış tarihi hakkında resmi bir açıklama yapılmadı.
Ekim 2025'teki çöküşü hatırlayan biri olarak bu haberi ilk okuduğumda temkinliydim. Ama bu kez fark şurada: kanıtlar herkesin indirip çalıştırabileceği Lean sertifikalarıyla geliyor ve geçen seferki iddiayı çürüten kişi bizzat bu sonucu ciddiye alıyor. Yine de "hakemli dergide yayımlandı" ile "basın bülteninde duyuruldu" arasındaki farkı unutmamakta fayda var — bu hikayenin sonunu önümüzdeki aylarda göreceğiz.