OpenAI math deposu: 722 makale, 372 aile ve Lean ile doğrulama yarışı

6 Ekim 2026 akşamı GitHub üzerinde beliren koleksiyon, matematik gündemini bir anda değiştirdi. OpenAI, herkese açık depoda 722 makaleyi 372 sonuç ailesi halinde yayımladı. Üretici, şirketin yayınlanmamış iç modeli olarak tanıtıldı. Ölçek kadar iddia da büyük: sayı teorisinden geometriye, kuramsal bilgisayar biliminden fizik-matematiğe uzanan 17 alan. Bu yazı, depoyu klonlayıp katalog, makale ve Lean izlerini okuyarak neyin var neyin yok sorusuna yanıt arıyor. OpenAI duyurusu, sürecin şeffaf yürütüldüğü tezini işliyor.

722 ile 372 aynı şey değil. Makale tek belge, sonuç ailesi ise aynı hedefe yürüyen belgelerin demeti: ana sonuç, eşlikçi gerekçe, uygulama ya da ikinci bir gerekçelendirme. Katalog en yüksek 377 sayısını taşıyor, aralarda 045, 061, 070, 123 ve 163 yok. Yani 372, dizin sayımından gelen gerçek toplam. Makalelerin tarihleri 10 Eylül ile 6 Ekim arasına yayılıyor; 6 Ekim yalnız katalogun çıkış günü. İncelenen kopya adc7f1241 commitine ait. Bu ayrımı Kingy derlemesi net kuruyor.

Sayılar ne anlatıyor

Üretim düzeni tek tip anlatılıyor. Model, doymuş ölçümlerin ardından açık problemlere yönelmiş, yaklaşık 4.000 problem önüne konmuş. Önem süzmesinden geçenler aile ve makale olarak derlenmiş. Sonuç başına ortalama 3 saat ChatGPT Pro düşünme süresi verilmiş. İki çalışma bu düzenin dışında tutulmuş: Riemann zeta için sıfır bölgesi ve CM abel çeşitlemelerde Hodge. Re(s) > 11/12 yazımı okunabilirlik için insan eliyle düzenlenmiş. Toplam $ tutar, jeton sayısı ve hızlandırıcı saati açıklanmadı. CellCog özeti, maliyet tarafındaki bu boşluğu açıkça işaret ediyor.

Depo turu üç duraktan oluşuyor. Önce overview kataloğu: 372 ailenin kısa tanımı ve bağlantıları. Sonra CONTENTS haritası: aileden makaleye geçiş. Son durak preprints dizinleri: her birinde PDF, kaynak metin ve alıntı bilgisi. Lisans Apache 2.0. Sürüm disiplini korunuyor, düzeltme yeni sürüm olarak ekleniyor. Tek makale indirmek yetiyor; tamamını klonlamak 2,4 GB ve 130 binden fazla dosya demek. BigChange envanteri, 722 dizinin her birinde PDF bulunduğunu doğruluyor.

Öne çıkan başlıklar

Sayı teorisi vitrini kalabalık. Aile 002, düşük Selmer derecesinde tam Birch–Swinnerton-Dyer formülü ve Tate–Shafarevich sonluluğu öne sürüyor. Aile 003, Dirichlet L işlevlerinin Re(s) > 7/8 yarı düzleminde sıfır taşımadığı tezi ve 11/12 için ikinci bir gerekçelendirme sunuyor. Aile 005 Catalan sabitinin irrasyonelliğini, aile 017 pi sayısının irrasyonellik üssünün 2 olduğu tezini işliyor. Flint–Hills toplamının yakınsaması da aynı demette. İki nokta Chowla ve Deligne–Drinfeld de listede. OpenAI kataloğu, bu başlıkları ispatlanmış gibi sunuyor.

Geometri ve fizik kanadı da geniş. Aile 032, CM abel çeşitlemeler ve K3 çarpımları için rasyonel Hodge tezini, Tate ve Hodge standardına uzanan sonuçlarla veriyor. Simetrik ve genel Mahler önermeleri aile 087’de. Karakteristik 2’de Kaplansky doğrudan-sonluluk tezine karşı örnek aile 197’de. Kuantum Heisenberg mıknatısılığında kendiliğinden mıknatıslanma 271’de, 3B relativistik Vlasov–Maxwell 362’de, serbest grup etmenlerinin eş yapılı olduğu tezi 287’de. Her biri uzun gerekçe zinciri isteyen, insan eliyle ayda zor okunan metinler.

Kuramsal bilgisayar bilimi en kalabalık küme: 40 aile. Unique Games önermesi, log-uzayda rastgeleliğin ek güç vermediği tezi (L = RL = BPL), matris çarpım üssü için 9/4 üst sınırı, n log n eşiğinin eşiğinde kalan tamsayı çarpımı ve Fourier dönüşümü iddiaları bu kümede. Thompson F grubunun yola gelmezliği, Hilbert–Smith, 3 ve 4 boyutta Kakeya, düzlemin 5 renkle birim-mesafe koşulunda boyanamayacağı tezi de aynı rafta. Kingy sayımına göre kombinatorik 37, geometri 36, sayı teorisi 31 aile taşıyor. Genişlik, denetim yükünü de büyütüyor.

Doğrulama ve tartışma

Biçimsel kanıt tarafı en dikkatli okunması gereken yer. CellCog sayımına göre 162 makalenin ana sonucu Lean anlatımına kavuşmuş. Kapsam belgeleri 235 aileyi çevreliyor. Yığın çok büyük: yaklaşık 122 bin Lean dosyası, 26 milyon satır, 30 dolayında dış biçimleme çalışmasından yararlanılmış. Denetim Comparator aracıyla koşuluyor; sınanan beyan ayrı, çözüm ayrı modülde duruyor. Meydan okuma beyanındaki sorry işareti, bitmemişlik değil eşlenecek beyanın yer tutucusu. Örnek yapılandırmada nanoda kapalı, yalnız üç standart aksiyom açık. Katalogdaki durum notları partial progress ve unchecked diyor. BigChange incelemesi, bu notların yayın üstverisi olduğunu, çalıştırılmış bir denetimin sonucu olmadığını vurguluyor.

Yöntem tartışması sonuç kadar önemli. IAS bünyesindeki bağımsız AGMAI, 9 isimden oluşuyor: Gowers, Witten, Hairer, Vakil, Wood ve diğerleri. Grup 29 Eylül’de 600’ü aşkın yanıtın ardından ilkeleri yayımladı: kapalı modellerle ileri problem yoklama yapılmasın, sonuçlar toplulukla birlikte sunulsun. 6 Ekim akşamı grup, danışmanlığın onay anlamına gelmediğini, yayının insan anlayışının başlangıcı olduğunu yazdı. OpenAI, revizyon ve alıntı kuralları ile topluluk barındırma arayışını duyurdu, çalıştaylara destek sözü verdi. AGMAI çizgisi net: erişim eşitlenmeden özgür araştırma olmaz.

Okura pratik rota şöyle. Önce overview kataloğunda ailenin kısa tanımını bul, sonra preprints dizininde ilgili makalenin PDF ve alıntı bilgisini sabitle: commit kimliği, dizin adı, sürüm. Kapsam belgesi varsa hangi beyanın Lean ile çevrelendiğini, nelerin dışarıda bırakıldığını not et. Lean’den geçen beyan güçlü sinyal, ama tek başına kabul anlamına gelmez; biçimsel beyan ile makaledeki tezin aynı olup olmadığına bak. Sıra bu: katalog, makale, Lean izi, bağımsız kaynak. Doğrulanmadan alıntılama. OpenAI, modeli sorumlu biçimde paylaşma hedefini yineliyor; AGMAI ise ölçüyü camianın vereceğini söylüyor.