گوگل ڈیپ مائنڈ کا AlphaProof Nexus: 56 سال سے حل نہ ہونے والے ریاضی کے مسئلے AI نے حل کر دیے

اہم نکات:

• گوگل ڈیپ مائنڈ کے نظام AlphaProof Nexus نے جدید لسانی ماڈلز کو Lean نامی ثبوت-جانچنے والے سافٹ ویئر کے ساتھ جوڑ کر ریاضی کے حل طلب مسئلے خودکار طریقے سے حل کیے ہیں
• 353 میں سے 9 ایردوش مسئلے حل کیے گئے، جن میں دو ایسے تھے جو 56 سال سے حل نہیں ہو سکے تھے
• 492 میں سے 44 عددی تسلسلوں (OEIS) کے مفروضے ثابت کیے گئے، اور اصلاح نظریہ (optimization theory) میں بھی پیش رفت ہوئی
• ہر مسئلے کی لاگت صرف چند سو ڈالر بتائی گئی ہے؛ ہر ثبوت کا ہر قدم مشین نے جانچا، اس لیے غلط بیانی کی گنجائش نہیں
• تنقیدی نکتہ: ماہرین کا کہنا ہے کہ ان ثبوتوں کی آزاد تصدیق ابھی باقی ہے؛ ڈیپ مائنڈ کے سربراہ ڈیمس ہاسابس کے بقول یہ نظام “اب بھی AGI نہیں”

مصنوعی ذہانت سے غلطی کی توقع رکھی جاتی ہے — وہ روانی سے جھوٹ بول دیتی ہے۔ مگر ریاضی وہ میدان ہے جہاں جھوٹ چلتا نہیں: ثبوت یا تو درست ہے یا نہیں۔ گوگل ڈیپ مائنڈ کی ٹیم نے اسی اصول کو ہتھیار بنایا ہے۔ ان کے نظام AlphaProof Nexus کی تفصیل 8 اکتوبر 2026 کو شائع ہونے والی تحقیق میں سامنے آئی، جس کے مطابق یہ نظام لسانی ماڈل کی تخلیقی صلاحیت کو Lean نامی سافٹ ویئر سے جوڑتا ہے — Lean ایک ایسا پروف اسسٹنٹ ہے جو ثبوت کے ہر منطقی قدم کو میکانیکی طور پر جانچتا ہے۔ ماڈل ثبوت کا مسودہ لکھتا ہے، کمپائلر غلطیاں واپس بھیجتا ہے، اور یہ غلطیاں اگلی کوشش کی رہنمائی کرتی ہیں۔ یہ چکر اس وقت تک چلتا ہے جب تک ثبوت منظور نہ ہو جائے یا نظام ہار نہ مان لے۔

نشانہ بنائے گئے مسئلے معمولی نہیں تھے۔ پال ایردوش ہنگری کے وہ ریاضی دان تھے جنہوں نے سینکڑوں ایسے سوال چھوڑے جو بیان کرنے میں آسان مگر حل کرنے میں ظالمانہ حد تک مشکل ہیں — ان میں سے کئی دہائیوں سے ریاضی دانوں کے لیے ایک مستقل امتحان بنے ہوئے ہیں۔ AlphaProof Nexus نے ان میں سے 353 باقاعدہ شکل دیے گئے مسئلوں میں سے 9 حل کیے۔ دو مسئلے تو 1970 سے حل طلب تھے، یعنی 56 سال سے انسانی ذہانت ان کے سامنے بے بس تھی۔ اس کے علاوہ آن لائن انسائیکلوپیڈیا آف انٹیجر سیکوینسز کے 492 مفروضوں میں سے 44 ثابت کیے گئے، الجبرائی جیومیٹری کا 15 سال پرانا ایک سوال حل ہوا، اور اصلاح نظریہ میں ایک معلوم حد کو بہتر بنایا گیا۔

سب سے حیران کن بات لاگت ہے: ہر حل شدہ مسئلے پر صرف چند سو ڈالر کے کمپیوٹ خرچ کا دعویٰ کیا گیا ہے۔ موازنہ کریں تو ایک محقق کی برسوں کی محنت کے مقابلے میں یہ رقم نہ ہونے کے برابر ہے۔ اور طریقہ کار کی سادگی بھی قابل غور ہے — ٹیم نے چار مختلف پیچیدگیوں کے ورژن بنائے، مگر نو کے نو ایردوش مسئلے سب سے سادہ ورژن نے حل کیے: ایک عام ماڈل اور کمپائلر کا چکر، جس میں علامتی فیڈبک ایمانداری کی ضمانت دیتا ہے، نہ کہ رواں عبارت۔

مگر کہانی کا دوسرا رخ بھی ہے، اور اسے نظر انداز نہیں کرنا چاہیے۔ مشین سے جانچا ہوا ثبوت رسمی درستگی کی ضمانت دیتا ہے، مگر یہ نہیں بتاتا کہ مسئلہ واقعی حل طلب تھا یا متعلقہ لٹریچر میں پہلے سے حل شدہ — اور نہ یہ کہ نظام نے کوئی اصل تصور پیش کیا یا صرف معلوم تکنیکوں کو نئے سرے سے جوڑا۔ معروف ریاضی دان ٹیرنس ٹاؤ کی رائے رپورٹ کے مطابق AI نظام موجودہ طریقے جوڑنے میں ماہر ہیں، مگر جہاں اصل تصور درکار ہو وہاں رک جاتے ہیں۔ ان کا تجویز کردہ اگلا قدم واضح ہے: ریاضی دانوں کو آزادانہ طور پر تصدیق کرنا ہو گی کہ یہ مسئلے واقعی حل طلب تھے اور ثبوت اصل ہیں۔

یہی وجہ ہے کہ ڈیمس ہاسابس نے خود توقعات کو قابو میں رکھا — ان کے الفاظ میں یہ نظام “اب بھی AGI نہیں”۔ یہ کوئی عام سوچنے والی مشین نہیں، بلکہ ایک محدود ورک فلو ہے جس میں AI کے خیالات کو غیر معمولی سختی سے جانچا، مسترد یا تصدیق کیا جا سکتا ہے۔

پاکستانی قارئین کے لیے اس خبر کی اہمیت دو سطحوں پر ہے۔ پہلی، یہ مصنوعی ذہانت کی اس نئی لہر کی مثال ہے جہاں AI صرف چیٹ نہیں کرتا بلکہ سائنسی تحقیق میں حصہ لیتا ہے — اسی سلسلے کی ایک اور مثال جاپان کا نینو-اے آئی ڈیوائس ہے۔ دوسری، یہ مصنوعی ذہانت کی ٹریننگ جیسی پیش رفتوں کے ساتھ مل کر بتاتی ہے کہ تحقیقی کام کی معیشت بدل رہی ہے: وہ کام جو برسوں لیتا تھا، اب مہینوں یا دنوں میں ہو سکتا ہے۔ ہماری جامعات کے لیے سوال یہ نہیں کہ AI ریاضی دانوں کی جگہ لے گا یا نہیں — سوال یہ ہے کہ جو محقق Lean جیسے اوزار سیکھے گا، وہ ان مسائل پر پہلے ہاتھ ڈالے گا جنہیں آج کوئی چھوتا نہیں۔