Science· 2026Q1
Yapay Zeka Ajanı, Resmi Kanıt Araması Kullanarak Açık Matematik Problemlerini Çözdü
Advancing mathematics research with AI-driven formal proof search
- 3atıf
- Q1SCImago
- 2026yıl
Kısa özet
Bir yapay zeka ajanı, büyük dil modelinin (LLM) kanıt üretimini Lean'deki resmi doğrulama ile birleştirerek 9 açık Erdős problemini ve 44 OEIS (Tam Sayı Dizileri Çevrimiçi Ansiklopedisi) varsayımını otonom olarak çözdü.
Yapay zekâ ile başlık ve abstract'tan üretildi; tam metin okunmaz.
Ana noktalar
- Yapay zeka ajanı, 353 açık Erdős probleminin 9'unu başarıyla çözdü.
- Yapay zeka ajanı, OEIS (Tam Sayı Dizileri Çevrimiçi Ansiklopedisi) varsayımlarının 492'sinin 44'ünü kanıtladı.
- Yöntem, LLM tabanlı kanıt üretimini Lean'deki resmi doğrulama ile birleştiriyor.
- Ajan, kombinatorik, optimizasyon ve kuantum optiği gibi araştırma alanlarında kullanıma sunuluyor.
Yapay zekâ ile başlık ve abstract'tan üretildi; tam metin okunmaz.
Özet (abstract)
Large language models (LLMs) increasingly excel at mathematics tasks, but their unreliability limits their utility in mathematics research. A mitigation is to use LLMs to generate formal proofs in languages such as Lean, in which the compiler verifies every proof step. We present the first demonstration of this method’s value in solving open problems at scale. We built an artificial intelligence agent for formal proof search that autonomously resolved nine of 353 open Erdős problems, proved 44/492 On-Line Encyclopedia of Integer Sequences conjectures, and is being deployed in combinatorics, optimization, graph theory, algebraic geometry, and quantum optics research. Even a basic agent alternating LLM-based generation with Lean-based verification replicated the Erdős successes. These findings demonstrate the power of formal proof search as an enabler of autonomous mathematical discovery.
Yazarların özeti; kaynağından alınmıştır. Science, 2026 · DOI ↗
Ücretsiz hesapla devam et
Makaleye Sor ile bu makaleye günde 3 soru ücretsiz; makaleyi kaydet, kaynakçasını al, ilgi alanına göre her gün yeni özetler. Çıkarımlar Premium.
Web'de ücretsiz devam etGoogle ya da Apple hesabınla giriş; kart istemez. Bu makaleye geri dönersin.
Telefonda:
Alan: Hesaplamalı Kuram ve Matematik
Computational Theory and MathematicsComputer Science