پوانکارے، مشین نے سطر سطر جانچیا

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

اک سنگھنا ثبوت، اک گواچی لائبریری

پوانکارے دا اندازہ، جیہنوں پیرلمین نے ثابت کیتا، آکھدا اے پئی ہر بند، سادہ جُڑیا (simply connected) تن پسارا مینیفولڈ — سوکھی زبان وچ، اک محدود 3D خلا جیہدے وچ کوئی اجیہی موری نہیں جتھے کوئی گول دھاگا اٹک سکے — تن پسارے گولے دے برابر اے۔ ثبوت رچرڈ ہیملٹن دے شروع کیتے ریچی فلو (Ricci flow) پروگرام اُتے چلدا اے۔ پیرلمین دے 2002–2003 دے تن پری پرنٹاں نے اہم دلیلاں بہت سنگھنی شکل وچ دتیاں؛ مفصل بیان مگروں آئے، جیہناں وچ جان مورگن تے گینگ تیان دا 2007 دا مونوگراف وی اے جیہدے پچھے ایہ منصوبہ چلدا اے۔

ایہ ثبوت جیومیٹرک تجزیے (geometric analysis) اُتے ٹکیا اے جیہڑا Lean دی برادری دی لائبریری Mathlib وچ بہتا نہیں سی۔ بہتیاں بنیاداں مُڈھوں بنانیاں پئیاں۔

ریاضی داناں دے جمائے سنگ میل

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

ستمبر 2026 وچ، اوہناں نے مُڑ شروع کیتا۔ ثبوت نوں لگ بھگ 90 سنگ میلاں (milestones) وچ کٹیا گیا، ہر اک لوڑیندیاں تعریفاں نال اک ٹھیک Lean بیان سی۔ ریاضی داناں نے ایہ بیان رسمی بنائے جان توں پہلاں یا دوران جانچے، تے فیر اوہ جما دتے گئے: ایجنٹ اوہناں نوں بدل نہیں سکدے سن، تے ہر درستی ریاضی داناں راہیں ای مُڑدی سی۔ کیوں جے کوئی وی ایجنٹاں دی لکھی ہر سطر نہیں پڑھ سکدا سی، ایہ سنگ میل اوہ جانچ چوکیاں بن گئے جتھے انساناں نے ریاضی دی تصدیق کیتی۔

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

لگ بھگ دو ہفتیاں وچ 2.8 ملین سطراں

مہینیاں دی تیاری مگروں، اصل رسمی کم دو ہفتیاں توں تھوڑا ودھ چلیا۔ اے آئی سبسکرپشناں تے کرائے دے سرورز اُتے لگ بھگ 25,000 ڈالر لگے۔ ایہ کم تھیورم دے ٹوپولوجیکل تے سموتھ دوہاں روپاں نوں ثابت کردا اے، پورا کمپائل ہوندا اے تے صرف Mathlib نال لکھے نشانہ بیاناں دے مقابلے اک آزاد جانچ وچوں لنگھدا اے۔

ایہ بہت وڈا اے: Lean دیاں لگ بھگ 3.2 ملین سطراں، جیہڑیاں صرف اوہ رکھ کے 2.8 ملین کیتیاں گئیاں جیہناں اُتے آخری تھیورم ٹکیا اے۔ لکھاریاں دی گنتی موجب، لگ بھگ ادھا پچھوکڑ دی تھیوری اے۔ اک کلاسیکی نتیجہ جیہدا ذکر مورگن تے تیان اک اکلے فٹ نوٹ وچ کردے نیں — تن پسارے مینیفولڈاں اُتے سموتھ ڈھانچیاں بارے — اکلا ای لگ بھگ 650,000 سطراں لے گیا۔

انساناں نے ہالے وی کیہ کیتا

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

جانچیا ہویا، پر ہالے سُتھرا نہیں

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

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