OpenAI, yayımlanmamış Astra modelinin on açık matematik probleminde sonuç ürettiğini duyurdu

Ne oldu?#

OpenAI 1 Ağustos 2026'da yayımladığı raporda, kamuya açılmamış Astra modelinin dahili bir sürümüyle uzun süredir açık duran on problemde yeni sonuçlar elde ettiğini bildirdi. Rapor her sonucun yanında modelin akıl yürütme adımlarının dökümünü ve Lean 4 ile yazılmış biçimsel kanıt dosyalarını taşıyor. Depo Apache-2.0 lisansıyla GitHub'da açık; Lean çekirdeği bir kanıtı ya kabul ya da reddettiği için doğrulama yapmak isteyenin modele erişmesi gerekmiyor, derleyiciyi çalıştırması yetiyor.

Listede yüksek boyutlu geometri ve teorik bilgisayar biliminden başlıklar var: 1999'dan beri açık duran sofik olmayan grup sorusu, Connes katılık varsayımı, 1978'den beri kırılamayan küre paketleme sınırı, Erdős problemlerinden 146, 180 ve 183, ikili ve küresel kod sınırları, aritmetik devre karmaşıklığı, kuantum paralel tekrar, en yakın vektör problemi ve Ehrhart hacim varsayımı. OpenAI araştırmacısı Noam Brown problem başına fazla harcama yapılmadığını ve listede "henüz" Milenyum Problemi bulunmadığını belirtti. erdosproblems.com sitesini yürüten Manchester Üniversitesi'nden matematikçi Thomas Bloom sonuçları X'te "büyük haber" diye niteledi.

Neden önemli?#

Dil modellerinin matematik iddiaları bugüne kadar çoğunlukla sınav benzeri ölçütlerle sunuluyordu. Bu duyurunun farkı, çıktının biçimsel bir kanıt diline çevrilmiş ve makinece denetlenebilir olması. Lean sertifikası "model doğru cevabı ezberlemiş olabilir mi" sorusunu ortadan kaldırmıyor ama "kanıt mantıksal olarak tutarlı mı" sorusunu kapatıyor. Değerlendirme tartışmasında bu, satıcının kendi bildirdiği benchmark tablosundan farklı bir kanıt türü.

Duyurunun en tartışmalı kısmı ise maliyet rakamı. OpenAI on çözümün token maliyetini Sol API fiyatlarına göre yaklaşık 2.000 dolar olarak veriyor; bu rakam başarısız denemeleri içermiyor ve model kamuya açık olmadığı için üçüncü taraflarca yeniden üretilemiyor. Duyuru bir ürün lansmanı da değil: Astra için erişim tarihi, fiyat listesi veya model kartı paylaşılmadı. Elde kalan tek bağımsız doğrulanabilir malzeme, Lean kanıt dosyaları.

Teknik ayrıntı#

• Depo Lean 4.32.0, mathlib kütüphanesi ve Lake derleme sistemiyle kurulmuş; sertifikalar yerelde önbellek çekip derleme çalıştırılarak doğrulanabiliyor.
• Doğrulama modele değil derleyiciye bakıyor: Lean çekirdeği bir kanıtı ya kabul eder ya reddeder, dolayısıyla Astra'ya erişimi olmayan biri de sonucu sınayabilir.
• Rapor 249 sayfa ve Ağustos 2026 tarihli; depo Apache-2.0 lisansıyla yayımlandı.
• Maliyet tahmini yaklaşık 2.000 dolar ve Sol API fiyatlarına göre hesaplanmış; yalnızca yayımlanan on çözümün token maliyetini kapsıyor, başarısız denemeler dahil değil.
• Astra'nın ağırlıkları, API erişimi veya bağımsız test arayüzü yayımlanmadı; sonuçların hiçbiri hakem değerlendirmesinden geçmedi.

Kimleri etkiliyor?#

Sinaptik yorumu#

Buradaki asıl yenilik bir modelin matematik yapması değil, iddianın denetlenebilir biçimde sunulması. Lean sertifikası, teknoloji basınında alışık olduğumuz "şu ölçütte şu skor" cümlesinden farklı bir kanıt standardı öneriyor ve bu standardın yaygınlaşması sektörün lehine olur. Ancak sertifika, biçimselleştirilen ifadenin doğru problemi kodladığını ve sonucun literatürde gerçekten açık olduğunu garanti etmez; o iş hâlâ insan hakemlerde. Model kamuya kapalı kaldığı sürece "Astra şunu yapabiliyor" cümlesi, OpenAI'ın kendi ölçümüne dayanan bir iddia olarak kalır.