OpenAI'ın Astra modelinin, yaklaşık 2.000 dolarlık işlem gücüyle on yıllardır açık kalan matematik problemini çözdüğü iddia edildi

OpenAI, Astra adını verdiği dahili ve henüz yayınlanmamış bir modelin, matematik ve teorik bilgisayar bilimlerindeki on açık problem için — bazıları onlarca yıldır çözümsüz kalmıştı — tamamen makine tarafından doğrulanmış kanıtlar ürettiğini ve toplam çıkarım maliyetinin kabaca 2.000 dolar olduğunu söylüyor. Bu rakamlar, şirketin 1 Ağustos 2026'da yaptığı duyuruyu aktaran, 10 Ekim 2026'da yayınlanan bir dev.to haberine dayanıyor.

OpenAI'nin yayınladıkları

dev.to haberine göre şirket, alanın bu iddiayı körü körüne kabul etmesini istemedi. Duyurunun yanı sıra 249 sayfalık bir metin ve temelindeki Lean 4 kanıt sertifikalarını GitHub'da Apache 2.0 lisansıyla yayınladı. Lean, her mantıksal adımı insan yargısına dayanmak yerine mekanik olarak denetleyen bir kanıt asistanıdır; depodaki "sorry" sayısının — Lean'ın kanıtlanmamış bir boşluğu işaretlemek için kullandığı gösterge — on sonuç boyunca sıfır olduğu bildiriliyor. Başka bir deyişle, her kanıttaki her biçimselleştirilmiş adımın doğrulandığı belirtiliyor.

Listelenen sonuçlar

Haber on problemden yedisini açıkça sayıyor:

• Sofik olmayan grupların varlığı. Astra'nın herhangi bir sonlu kümeyle yaklaşılamayan belirli bir grup inşa ettiği, böylece Mikhail Gromov'un 1999'da sofikliği tanımlamasından beri açık olan bir soruyu çözdüğü ve bunun 27 yıldır ilk somut karşı örnek olduğu bildiriliyor.
• İyileştirilmiş bir küre paketleme sınırı; yüksek boyutlu küre paketleme yoğunluğu için genel üst sınırdaki ilk ilerleme olarak nitelendiriliyor — 1978'den beri, yani 48 yıllık bir tavan.
• Von Neumann cebirleriyle ilgili uzun süredir savunulan Connes'ın kararlılık konjektürünü çürüten bir karşı örnek.
• Ehrhart'ın hacim konjektürünün bir kanıtı.
• Paul Erdős'ün açık problem kataloğundan üç problem; bunlar arasında çok renkli Ramsey sayılarıyla ilgili 183 numaralı problem de var.

Kalan üç sonuç kaynakta tek tek sıralanmamış.

Fiyat etiketinin neden dikkat çektiği

dev.to yazısına göre ilginç olan sayı modelin adı değil, oran: Uzman matematikçilere 48 yıla kadar direnen soruların, bu anlatıya göre, bir hafta sonu GPU kiralamasından daha küçük bir işlem faturasıyla kapatılmış olması. Buradaki çerçeve, Astra'nın bu problemlere yıllarını harcayan insanlardan daha zeki olduğu değil; kanıt uzayını makine hızıyla tarayabilen ve her adımı Lean tarafından doğrulanan bir sistemin, aksi halde yıllarca sürecek bir araştırma çabasını kısa ve ucuz bir çalışmaya sıkıştırabileceği.

Tepkiler ve eksik adım

Haberde aktarılan tepkiler olumlu ama ölçülü. Fields Madalyası sahibi Timothy Gowers olumlu bir tepki verirken alanın sonuçları hâlâ sindirdiğini belirtti. Erdős'ün açık problemlerinin genel bir veritabanını yöneten Thomas Bloom, bu on sonucu X'te "büyük haber" olarak nitelendirdi ve bunları, OpenAI'nin önceki bir dahili modelinin Mayıs 2026'da ürettiği birim mesafe karşı örneğinin üzerine koydu.

Haber sınırlılık konusunda da aynı derecede açık: on kanıttan hiçbiri henüz resmi hakemli incelemeden geçmedi. Lean doğrulaması bir kanıtın kendi içinde tutarlı olduğunu gösterir; makine tarafından denetlenmiş bir argümanı kabul görmüş matematiğe dönüştüren topluluk incelemesinin yerine geçmez. Ayrıca buradaki her şeyin, OpenAI'nin duyurusuna ilişkin tek bir ikincil habere dayandığını, bağımsız bir haber kapsamı bulunmadığını da belirtmek gerek.

Tek seferlik değil, bir örüntü

Yazı bu sonucu bir dizide konumlandırıyor. GPT-5.6 Sol'unun Temmuz 2026'da 50 yıllık bir konjektürü çözdüğü, Mayıs 2026'daki karşı örneğin ise ondan önce geldiği bildiriliyor. Bu okumaya göre öncü laboratuvarlar biçimselleştirilmiş matematiğe yöneliyor; çünkü bir kanıt denetleyicisi sahtelenemez bir geçti/kaldı sinyali sağlıyor — bu da bir modelin yayımlanmış çalışmaları getirip yeniden birleştirmek yerine özgün araştırma yapabildiğini göstermenin görece temiz bir yolu.

Neden önemli

Bildirilen sonuçlar geçerliliğini korursa, özgün ve doğrulanabilir matematik üretmenin maliyeti katbekat düşmüş olur ve darboğaz kanıt üretmekten bunları incelemeye kayar. İzlenecek sorular şunlar: on kanıttan herhangi biri tam hakemli incelemeden değişmeden çıkabilecek mi ve Astra ya da nihai kamu sürümü, laboratuvarın kendisinin seçtiği değil dışarıdaki matematikçilerin seçtiği problemlerde bu performansı tekrarlayabilecek mi. O zamana kadar bu, biçimsel doğrulamanın büyük ölçekli model aramasıyla birleşince neyi başarabileceğinin çarpıcı ama henüz incelenmemiş bir gösterimi olarak duruyor.