لگتا ہے کہ مصنوعی ذہانت تقریباً ہر ہفتے ایک نیا ریاضی کا مسئلہ حل کر رہی ہے۔ پچھلے ماہ، صرف OpenAI نے 719 مسودے جاری کیے جن میں اس شعبے کے کچھ سب سے مشکل مسائل حل ہونے کا دعویٰ کیا گیا۔ حتیٰ کہ کمپیوٹر کی جانچ میں بھی غلطی ہو سکتی ہے۔ کئی سالوں تک AI کے زائد اور بے کار مواد کے بعد، لوگ یہ پوچھنا شروع کر دیتے ہیں کہ کیا ریاضی اگلا متاثرہ شعبہ بن جائے گا۔
ایکسیوم میتھ کو اس قسم کی قسمت سے بچنے کے لیے تیزی سے کم کرنے کے بجائے زیادہ مضبوط بنیاد بنانی ہوگی۔ اس 16 ارب ڈالر کی قیمت والی اسٹارٹ اپ کا مقصد ایک تصدیق شدہ بنیادی تہہ تعمیر کرنا ہے جس پر AI ایجنسز انحصار کرکے سافٹ ویئر لکھ سکیں اور آخرکار سائنسی تحقیق کر سکیں۔
ہفتہ کو، کمپنی نے اعلان کیا کہ اس نے اسٹیکس پروجیکٹ کی تصدیق کر لی ہے، جو انسانوں کے زیرِ نگرانی لکھے گئے بڑے ترین ریاضی کے نتائج میں سے ایک ہے۔ ریاضیدان عام طور پر اسٹیکس کو بہت اونچی قدر دیتے ہیں۔ کولمبیا یونیورسٹی کے ریاضیدان پیٹر ووٹ نے اسے “اس کے ساتھ تقریباً کچھ بھی موازنہ نہیں کیا جا سکتا” کہا اور اس پروجیکٹ کو مشہور بوربکی سیریز سے موازنہ کیا — وہ سیریز جو 20ویں صدی میں ریاضی کو بنیادوں سے دوبارہ تعمیر کرنے کے لیے شائع ہوئی تھی۔
وائٹ کے کولمبیا کے ساتھی جوہن دے یونگ نے 2005 میں ایک اوپن سورس رفرنس کے طور پر اسٹیکس پروجیکٹ شروع کیا۔ اس کے بعد، ریاضیدانوں نے اس میں مسلسل اضافہ کیا ہے، جس میں یونیورسٹی کے سطح کے الجبرا سے لے کر الجبرا، جیومیٹری اور نمبر تھیوری کے سب سے آگے کے خیالات تک شامل ہیں۔
اس کمپنی کے AI ایجینٹس نے اس 7,654 صفحات کے ڈیٹا بیس کو تقریباً 16 ملین لائنز کوڈ میں ترجمہ کر دیا جو کمپیوٹر کے ذریعے چیک کیا جا سکتا ہے۔
فرمیل ریاضی کا مقصد یہ یقینی بنانا ہے کہ اس کی بنیادی ساخت قابل اعتماد ہے۔ ریاضیدان اپنے ثبوت کو ایک لیان نامی پروگرامنگ زبان میں کوڈ میں تبدیل کرتے ہیں، اور پھر ایک ثبوت مددگار پروگرام ان کوڈز کو لائن بہ لائن چیک کرتا ہے۔ اگر ثبوت کامیاب ہو جائے، تو ریاضیدان اس پر یقین کر سکتے ہیں کہ یہ منطقی طور پر درست ہے۔
انجینئرز نے بھی اسی خیال، یعنی فارمال ویریفکیشن، کا استعمال کیا تاکہ چپ ڈیزائن کی ممکنہ حیثیت کی تصدیق کر سکیں؛ فرانسیسی تحقیق کاروں نے اس کا استعمال کرکے گھریلو سہولت کے لیے سافٹ ویئر میں خرابی کا پتہ لگایا۔
جیسے Stacks Project جیسے ذخیرہ کے لیے، مسلسل تھیورمز کی جانچ کرنا صرف کام کا ایک حصہ ہے۔ Stacks میں تھیورمز اور تعریفیں ایک دوسرے سے منسلک ہیں، اور ہر ایک پچھلے مواد پر مبنی ہوتی ہے۔ جیسے خاندانی درخت، Stacks میں بہت سے نتائج پچھلے نتائج تک جا کر گھل سکتے ہیں۔
اس متبادل تعلق کی وجہ سے ایکسیوم کو شروع میں یہ محسوس ہوا کہ یہ منصوبہ ممکن نہیں ہے۔ ٹیم کو تقریباً 16 ملین لائن لین کوڈ میں ہر کنکشن کو مکمل اور بحال رکھنا پڑا۔
ایکسیوم کے سی ای او کیرینا ہانگ نے ٹیک کرنش کو بتایا: "حجم اور دقت کا عملی زندگی میں عام طور پر مطابقت نہیں رکھتا۔ [اسٹیکس] ریاضی کی بنیاد بنانے والے ریاضی کے نتائج کا ایک مجموعہ ہے۔ آپ چاہتے ہیں کہ [نظریات] ایک دوسرے کے ساتھ مطابقت رکھیں، نہ کہ تضاد کی طرح۔ آپ چاہتے ہیں کہ ان تعریفوں کے درمیان بھی تضاد نہ ہو۔"
یہ 25 سالہ سی ای او نے اسٹینفورڈ یونیورسٹی کے ریاضی کے ڈاکٹریٹ پروگرام سے ڈراپ آؤٹ کیا اور 2025ء کے مارچ میں اس کمپنی کی بنیاد رکھی۔ اس سال مارچ میں، ایکسیوم نے مینلو وینچرز کی قیادت میں 2 ارب ڈالر کا A سیریز فنڈنگ مکمل کیا۔
ہونگ نے کہا: "ہم وقتاً فوقتاً یقین نہیں رکھتے تھے کہ وائب کوڈنگ Stacks کی خوبصورتی کو برقرار رکھ سکے گی۔"
اس منصوبے کو مکمل کرنے کے لیے، ٹیم نے ایجینٹس کے لیے ایک لمبی ساخت ڈالی اور انہیں متوازی طور پر چلایا۔ ایکسیوم ٹیکنالوجی ٹیم کے رکن اشون سوامیناتھن کہتے ہیں: "اسٹیکس کے لیے، ہم نے ایک ہائرارکی ترتیب دی… لیکن ایسی نہیں جو ہر ایجینٹ کو بالکل بتائے کہ وہ کیا کرے۔ ایجینٹس خود ٹاسک تلاش کرتے ہیں اور ان چیزوں کو پہچانتے ہیں جنہیں متوازی طور پر处理 کیا جا سکتا ہے۔"
ایکسیوم نے اپنے مدلز کو ریاضی میں ماہر بنانے کے لیے بھی تربیت دی ہے۔ ہانگ کہتے ہیں کہ یہ عمل زیادہ تر دوسری تصدیقی اسٹارٹ اپس نے اپنایا نہیں ہے۔ شروع میں، ٹیم نے ان ایجینٹس کو انسان جیسے ججمنٹ کے معیار بنانے کے لیے ایک اندر کے لین ایکسپرٹ پر انحصار کیا۔ وقت کے ساتھ، ہانگ کہتے ہیں، ان ایجینٹس نے خود یہ ججمنٹ سیکھ لیا۔
یہ کام فارمل ریاضی کے سب سے بڑے خالی مقامات میں سے ایک کو پُر کرتا ہے۔ سوامیناتھن کہتے ہیں: "جب آپ پہلے سے فارملائزڈ ریاضی کو دیکھتے ہیں، تو آپ کو ایک بہت بڑا سیاہ خلائیں نظر آتی ہے۔ اور وہ خالی جگہ الجبرائی جیومیٹری کو کور کرتی ہے۔"
سوامناتھن نے کہا کہ اب تک، لیان کا استعمال کرکے الجبرائی جیومیٹری کے نئے کام کی جانچ کرنے والے تحقیق کاروں کے پاس تقریباً کوئی تیار بنیادی ڈھانچہ دستیاب نہیں تھا۔ "اب ان کے پاس ہے۔"
اکسیوم کا خیال ہے کہ ہر تصدیق شدہ نتیجہ ایک ایسا اینٹ ہوتا ہے جس پر مستقبل کے ثبوت موجودہ تصدیق شدہ ریاضی کے بنیاد پر بنا جا سکتے ہیں، بغیر کہ دوبارہ شروع کرنے کے۔ یو سی ایل اے کے ریاضیدان اور فیلڈز میڈل وصول کنندہ تیرنس ٹاؤ نے اس بات کو مختصر الفاظ میں بیان کیا: "جتنا زیادہ آپ کے پاس فارملائزڈ ثبوت ہوں گے، آپ اتنے ہی زیادہ فارملائزڈ ثبوت بنانے میں کامیاب ہو سکتے ہیں۔"
ایکسیوم کا مقصد صرف ریاضیدانوں تک محدود نہیں ہے۔ ڈویلپرز طویل عرصے سے اپنے کوڈ میں خامیوں اور سیکیورٹی خطرات سے بچنے کی کوشش کر رہے ہیں۔ جبکہ AI ایجینٹس زیادہ سے زیادہ سافٹ ویئر لکھ رہے ہیں، یہ مسئلہ مزید بڑھتا جائے گا۔
اکسیم بیٹنگ، مستقبل کے سافٹ ویئر کو ابھی کے Stacks کی طرح تصدیق شدہ بنیادوں پر بنایا جانا چاہیے۔
سواتمناتھن نے کہا: "ہم سمجھتے ہیں کہ ریاضی وہ شعبہ ہے جہاں سے آپ ان چیزوں کو تعمیر کرنا شروع کرتے ہیں، اور یہ ایک قابل انتقال مہارت ہے۔ ایجنسیاں ہمارے کوڈ کو پڑھ سکتی ہیں، اسے سمجھ سکتی ہیں، اور اس پر نئی بنیادی ڈھانچہ تعمیر کر سکتی ہیں۔ ہم نے لین کے ساتھ جو فارملائزیشن کی ہے، وہی اب ایجنسیاں جس پر بنیاد رکھ سکتی ہیں، بنیادی ڈھانچہ ہے۔"
ایکسیوم کے ایجینٹس کی طرف سے اسٹیکس کی تعمیر کا طریقہ — جس میں وہ متوازی طور پر کام کرتے ہیں اور اپنے کام کا انتخاب کرتے ہیں — وہی ہے جو ہانگ نے مستقبل میں بہت سے AI کاموں کے لیے تصور کیا ہے۔ وہ سمجھتی ہیں کہ AI ایجینٹس کو بے رنگ مواد کو روکنے کے لیے ایک منظم، دوبارہ استعمال کی جانے والی معلومات کا خزانہ درکار ہے۔
ہونگ کہتے ہیں: "آپ چاہتے ہیں کہ [ایجینٹ] ایک قابل استعمال ڈیٹا بیس رکھے، جس پر وہ آگے بڑھ کر اپنی سرحدیں مزید بڑھا سکیں۔ اگر شروع میں بدترین انجینئرنگ کے فیصلوں کے ذریعے گندگی ڈال دی جائے، تو ان کے لیے اس سرحد کو مزید وسعت دینا مشکل ہو جائے گا۔"
ہونگ اس طریقہ کے بارے میں بہت زیادہ اعتماد رکھتی ہیں، اور انہوں نے علنی طور پر چیلنج جاری کیا۔ انہوں نے کہا: "میں تمام پروگرامنگ کمپنیوں کو علنی طور پر چیلنج کرتی ہوں کہ وہ اس سائز کا فارمل ورک کریں۔"