Google DeepMind, matematikçi Paul Erdős’ün ortaya attığı dokuz açık problemi çözen yapay zekâ sistemi AlphaProof Nexus’a ilişkin hakemli çalışmasını yayımladı. Makale 8 Ekim Perşembe günü Science dergisinde çıktı. Sistem ayrıca Tamsayı Dizileri Çevrimiçi Ansiklopedisi’ndeki (OEIS) 44 varsayımı da kanıtladı.

56 yıllık problemler çözüldü

Çözülen Erdős problemlerinden ikisi, 1970’te Erdős ve András Sárközy tarafından ortaya atılmıştı ve 56 yıldır yanıtsızdı. Sistem, cebirsel geometrideki dört açık problemden ikisini de çözdü; bunların arasında Zanello’ya ait bir sanı da var. DeepMind sonuçları ilk olarak mayıs ayında arXiv’de paylaşmıştı, Science yayını bunlara hakemli bir dayanak sağlıyor. Ön baskıya göre çözülen her Erdős problemi hesaplama maliyeti olarak birkaç yüz dolara mal oldu.

Sistem nasıl çalışıyor?

AlphaProof Nexus, kanıt aramak için Gemini 3.1 Pro’yu kullanıyor. Kanıtları ise Lean adlı kanıt asistanı denetliyor; Lean her adımı mekanik olarak doğruluyor ve boşluk içeren kanıtları reddediyor. Ekip 353 Erdős problemi ve 492 OEIS sanısı üzerinde çalıştı. OEIS’e ait 44 kanıt elle kontrol edilerek problemlerin doğru formalize edildiği ve daha önce kanıtlanmadığı doğrulandı. Dikkat çekici bir bulguya göre, yalnızca kanıt üretip bunu kontrol eden çok daha basit bir ajan sürümü de dokuz problemin hepsini çözdü.

Sınırlılıklar ve eleştiriler

Sistem denediği problemlerin çoğunda başarısız oldu. Bazı başarısız denemelerde ispatlayamadığı bir adımı atlamak için Lean’in “sorry” yer tutucusunu koydu ya da var olmayan teoremlere atıfta bulundu. Fizikçi Anatol Wegner, “açık” diye sunulan bazı problemlerin yayımlanmış çalışmalarda zaten çözüldüğünü savundu. Katalonya Açık Üniversitesi’nden Josep Curto Díaz sistemde hâlâ yapısal bir insan bağımlılığı olduğunu söyledi. DeepMind yazarlarından Swarat Chaudhuri ise sonuçların dikkatle gözden geçirilmesi gerektiğini belirterek “Sonuçta matematik, insani bir etkinliktir” dedi.