پوانکارے، مشین کے ہاتھوں سطر بہ سطر جانچا گیا

کسی ثبوت کی جانچ ریاضی کے سب سے کٹھن کاموں میں سے ایک ہے، خاص طور پر جب کوئی دلیل کئی شعبوں پر پھیلی ہو۔ جیسے جیسے اے آئی ثبوتوں کی تیاری کو تیز کرتی ہے، قابلِ اعتماد تصدیق کی اہمیت بڑھتی جاتی ہے۔ Lean 4 جیسے ثبوتی معاون (proof assistants) ایک جواب پیش کرتے ہیں: تعریفیں، بیانات اور ثبوت کوڈ کی شکل میں لکھے جاتے ہیں، اور سافٹ ویئر کا ایک چھوٹا قابلِ اعتماد مرکز، یعنی اس کا “کرنل”، ہر قدم کی جانچ کرتا ہے۔ کرنل سے گزر جانے والا ثبوت اپنے بیان کو ثابت کر دیتا ہے؛ انسانوں کے لیے بس یہ جانچنا باقی رہ جاتا ہے کہ بیان واقعی وہی کہتا ہے جو ریاضی دانوں کی مراد ہے۔

ایک مختصر ثبوت، ایک غائب لائبریری

پیرل مین کا ثابت کردہ پوانکارے کا قیاس کہتا ہے کہ ہر بند، سادہ طور پر مربوط سہ جہتی منی فولڈ — غیر رسمی طور پر، ایک محدود سہ جہتی فضا جس میں کوئی ایسا سوراخ نہ ہو جس میں کوئی پھندا اٹک سکے — سہ جہتی کرے کے مساوی ہے۔ یہ ثبوت رچرڈ ہیملٹن کے شروع کردہ رِچی فلو (Ricci flow) کے پروگرام پر چلتا ہے۔ پیرل مین کے 2002–2003 کے تین پری پرنٹس نے کلیدی دلائل نہایت مختصر شکل میں دیے؛ تفصیلی بیانات بعد میں آئے، جن میں جان مورگن اور گینگ تیان کا 2007 کا مونوگراف بھی شامل ہے جس کی یہ منصوبہ پیروی کرتا ہے۔

یہ ثبوت جیومیٹرک تجزیے پر انحصار کرتا ہے جو Lean کی کمیونٹی لائبریری Mathlib میں زیادہ تر موجود نہیں تھا۔ بنیادوں کا بڑا حصہ صفر سے تعمیر کرنا پڑا۔

ریاضی دانوں کے منجمد کیے ہوئے سنگِ میل

پیکنگ یونیورسٹی اور بیجنگ کے دیگر اداروں کے ژی یوان ژانگ، ایکسل دیلاوال، بن ڈونگ، چن لے لیو اور ان کے ساتھیوں نے مئی 2026 میں کام شروع کیا: ریاضی کی تربیت رکھنے والے تین “اے آئی انجینئرز” ریاضی دانوں کے ساتھ مل کر کام کر رہے تھے۔ ان کا پہلا طریقہ — پس منظر کے نظریے کے بڑے حصوں کو باضابطہ شکل دینا — سست تھا، اور نتیجے میں بننے والا کوڈ ان کی توقعات پر پورا نہیں اترا۔

ستمبر 2026 میں انہوں نے ازسرِنو آغاز کیا۔ ثبوت کو تقریباً 90 سنگِ میل میں بانٹا گیا، جن میں سے ہر ایک اپنی ضروری تعریفوں کے ساتھ Lean کا ایک درست بیان تھا۔ ریاضی دانوں نے ان بیانات کا ان کی باضابطہ تشکیل سے پہلے یا اس کے دوران جائزہ لیا، اور پھر انہیں منجمد کر دیا گیا: ایجنٹ انہیں بدل نہیں سکتے تھے، اور ہر تصحیح ریاضی دانوں کے ذریعے واپس جاتی تھی۔ چونکہ کوئی بھی ایجنٹوں کی لکھی ہر سطر نہیں پڑھ سکتا تھا، یہ سنگِ میل وہ جانچ کی چوکیاں بن گئے جہاں انسان ریاضی کی تصدیق کرتے تھے۔

پھر ایجنٹوں نے متوازی طور پر کام کیا، کوڈنگ ٹولز — زیادہ تر Codex اور Claude Code — کے ساتھ انٹرایکٹو سیشنز کے ذریعے، اور Archon Horizon نامی ایک نظام کے ذریعے جو محدود “مشنز” بہت سے سرورز پر بھیجتا ہے۔ ایک بوٹ ہر حصے کو کمپائل کرتا اور قبول شدہ حصوں کو ضم کرتا تھا۔ بیانات کی باضابطہ تشکیل اور ثبوتوں کی تعمیر کا زیادہ تر کام GPT-6-Astra نے کیا؛ Fable-5.1 کو آزادانہ جانچ، رکے ہوئے کاموں کی تشخیص اور بیانات کے جائزے کے لیے استعمال کیا گیا۔

تقریباً دو ہفتوں میں 28 لاکھ سطریں

مہینوں کی تیاری کے بعد اصل باضابطہ تشکیل میں دو ہفتوں سے کچھ زیادہ وقت لگا۔ اے آئی کی سبسکرپشنز اور کرائے کے سرورز پر تقریباً 25,000 ڈالر خرچ ہوئے۔ یہ کام مسئلے (theorem) کی ٹوپولوجیکل اور ہموار (smooth) دونوں صورتوں کو ثابت کرتا ہے، مکمل طور پر کمپائل ہوتا ہے اور صرف Mathlib کی مدد سے لکھے گئے ہدفی بیانات کے مقابلے میں ایک آزادانہ جانچ سے گزرتا ہے۔

یہ بہت بڑا ہے: Lean کی تقریباً 32 لاکھ سطریں، جنہیں صرف وہی رکھ کر جس پر آخری مسئلہ منحصر ہے 28 لاکھ تک کم کیا گیا۔ مصنفین کے حساب سے تقریباً آدھا حصہ پس منظر کا نظریہ ہے۔ ایک کلاسیکی نتیجہ جس کا مورگن اور تیان صرف ایک حاشیے میں ذکر کرتے ہیں — سہ جہتی منی فولڈز پر ہموار ساختوں کے بارے میں — اکیلے تقریباً 6,50,000 سطروں پر محیط ہوا۔

انسانوں نے اب بھی کیا کیا

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

تصدیق شدہ، مگر ابھی صاف ستھرا نہیں

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

مفادات کا ٹکراؤ۔ ٹیم نے Anthropic کے Claude Code اور Fable-5.1 ماڈل کو GPT-6-Astra کے ساتھ استعمال کیا، جو OpenAI کی سبسکرپشنز کے ذریعے استعمال ہوا اور جس نے زیادہ تر کام کیا۔ مقالہ اپنے منصوبے کا موازنہ Anthropic کی فرما کے آخری مسئلے کی باضابطہ تشکیل سے بھی کرتا ہے۔ یہ مضمون Claude نے لکھا ہے۔