Google DeepMind’in AlphaProof Nexus’u 9 açık Erdős problemini çözdü; çalışma Science’ta yayımlandı

Google DeepMind araştırmacılarının geliştirdiği AlphaProof Nexus, hakemli bilimsel dergi Science’ta 8 Ekim 2026’da yayımlanan “Advancing mathematics research with AI-driven formal proof search” başlıklı makaleyle akademik süzgeçten geçti. Makaleye göre sistem, denenen 353 açık Erdős probleminden 9’unu otonom olarak çözdü; bunlardan ikisi 56 yıldır yanıt bekliyordu. Sistem ayrıca On-Line Encyclopedia of Integer Sequences (OEIS) veritabanındaki 492 açık sanının 44’ünü kanıtladı.

AlphaProof Nexus nasıl çalışıyor?

Makalenin özetine göre büyük dil modelleri matematik görevlerinde giderek başarılı olsa da güvenilirlik sorunları araştırma matematiğindeki kullanımlarını sınırlıyor. Araştırmacıların çözümü, modele ispatları derleyicinin her adımı doğruladığı biçimsel ispat dili Lean’de yazdırmak. AlphaProof Nexus’un temel sürümünde Gemini 3.1 Pro tabanlı alt ajanlar bağımsız olarak ispat adımları üretiyor, Lean derleyicisi bunları denetliyor ve hata mesajları bir sonraki denemeye geri besleniyor. “Tam donanımlı” sürümde ise alt ajanlar AlphaEvolve’dan esinlenen evrimsel bir algoritmayla koordine ediliyor ve zor alt problemler için DeepMind’in olimpiyat düzeyindeki ispat aracı AlphaProof’u çağırabiliyor.

Dikkat çekici bulgulardan biri, yalnızca dil modeli ile Lean geri bildirimini dönüşümlü kullanan en basit ajanın da Erdős problemlerindeki dokuz başarının tamamını tekrarlayabilmesi. arXiv ön baskısına göre en zor problemlerde basit ajan daha pahalı kalıyor; tam donanımlı ajan problem başına “birkaç yüz dolarlık” çıkarım maliyetiyle sonuca ulaştı.

Erdős problemlerinin ötesinde

Ön baskıya göre sistem ayrıca cebirsel geometride Hilbert fonksiyonlarına ilişkin 15 yıllık bir soruyu yanıtladı, konveks optimizasyonda yeni bir algoritmik parametre takvimi bularak açık bir sınırı iyileştirdi, literatürdeki bazı hatalı biçimselleştirmeleri tespit etti ve Ben Green’in bilinen açık problemler listesinden birinin çözümüne yardımcı oldu. Kombinatorik, optimizasyon, graf teorisi, cebirsel geometri ve kuantum optik alanlarındaki araştırmalarda da kullanılıyor. Her Erdős çözümünden sonra ekipteki uzmanlar Lean ifadesinin orijinal sanıyı doğru yansıttığını doğruladı; sonuçlar Terence Tao’nun yapay zekânın Erdős problemlerine katkılarını kaydeden wiki sayfasına da işlendi. Başarılı Lean ispatları ve insan tarafından yazılmış doğal dil ispatları Google DeepMind’in GitHub deposunda herkese açık.

Sınırlar ve bağlam

Araştırmacılar başarıların Lean’in matematik kütüphanesi Mathlib’in olgun olduğu ve görevlerin yönetilebilir alt hedeflere bölünebildiği alanlarda yoğunlaştığını, Erdős problemlerinin büyük çoğunluğunun hâlâ erişilemez kaldığını kabul ediyor. Science’taki eşlik eden değerlendirme yazısında Jeremy Avigad ve Matthew Ballard, başarısız ispat denemelerinin bile matematikçilerin problemleri daha iyi anlamasına yardımcı olduğunu vurguladı. The Decoder, çalışmanın yapay zekâ matematiği konusundaki tartışmanın kızıştığı bir döneme denk geldiğini; OpenAI’ın yüzlerce yapay zekâ ispatını dergilere göndermek yerine GitHub’da yayımlamasının ardından bazı matematikçilerin boykot çağrısı yaptığını, DeepMind’in ise çalışmasını hakem değerlendirmesinden geçirdiğini hatırlatıyor.

Kaynak: Science: Advancing mathematics research with AI-driven formal proof search · arXiv ön baskısı · Google DeepMind: alphaproof-nexus-results (GitHub) · EurekAlert! (AAAS) · The Decoder