‏AlphaProof Nexus گوگل دیپ‌مایند: حل مسائل ریاضی دهه‌ها-پاسخ‌نداده

گوگل دیپ‌مایند یه فریم‌ورک جدید به اسم AlphaProof Nexus منتشر کرده که توانسته ۹ تا از ۳۵۳ مسئله‌ی باز مجموعه‌ی اِردوش رو به‌صورت خودکار حل کنه — از جمله دو سؤالی که از سال ۱۹۶۹ بی‌جواب مونده بودند. علاوه بر اون، ۴۴ تا از ۴۹۲ حدس باز از دانشنامه‌ی آنلاین دنباله‌های اعداد صحیح (OEIS) هم حل شدن. هزینه‌ی محاسباتی برای هر مسئله فقط چند صد دلار بوده، که در مقایسه با مقیاس مسائل، رقم قابل‌توجهیه.

ایده‌ی اصلی سیستم اینه که مدل زبانی — اینجا Gemini 3.1 Pro — نباید تمام زنجیره‌ی منطقی رو به‌تنهایی توی زبان طبیعی حمل کنه. به‌جاش، گام‌های اثبات رو توی Lean تولید می‌کنه؛ Lean یه زبان برنامه‌نویسی رسمیه که برای تأییدیه‌ی ریاضی طراحی شده. کامپایلر Lean هر قدم رو بررسی می‌کنه و اگه اشتباهی باشه، پیام خطا مستقیم به مدل برمی‌گرده تا دوباره تلاش کنه. این حلقه‌ی بازخورد نمادین، ضعف مدل‌های زبانی در استدلال منطقی رو تا حد خوبی جبران می‌کنه.