OpenAI کی 6 اکتوبر کی ریاضیاتی ریلیز عوام کے لیے 722 مسودوں کا مجموعہ پیش کرتی ہے، جسے نتائج کے 372 خاندانوں میں منظم کیا گیا ہے۔ ایک خاندان میں کئی مقالے ہو سکتے ہیں، جبکہ رسمی ثبوت کا دائرہ متعلقہ مسودے کے دعوے سے محدود تر ہو سکتا ہے۔ کسی مقالے کو ذخیرے میں اس کی ثبوتی ترتیب تک دیکھنے سے معلوم ہوتا ہے کہ جانچ کے لیے کون سا دعویٰ چنا گیا۔

7 اکتوبر کو BIG CHANGE نے ذخیرے کی مکمل فائل فہرست، کیٹلاگ اور منتخب ثبوتی فائلوں کا جائزہ لیا۔ یہ دستاویزات اور جامد فائلوں کا تجزیہ ہے؛ ہم نے Lean لائبریری مرتب نہیں کی، ثبوت جانچنے والا پروگرام نہیں چلایا اور ریاضی کی علمی جانچ نہیں کی۔ OpenAI کا اعلان ایک مسلسل ترقی کرتی ریلیز بیان کرتا ہے اور کہتا ہے کہ مزید رسمی صورتیں بعد میں آئیں گی۔

بڑی تبدیلی

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

مسودوں اور خاندانوں کو الگ الگ شمار کریں

ہماری فہرست میں preprints/ کے تحت 722 براہ راست مسودہ ڈائریکٹریاں ملیں، ہر ایک میں ایک PDF؛ جبکہ reasoning_traces/ کے تحت 10 PDF ملیں۔ مسودوں کا نقشہ خاندانوں کی 372 منفرد اندراجات اور 722 مسودوں کے روابط رکھتا ہے۔

یہ شمار مختلف چیزیں بیان کرتے ہیں:

فائل

قارئین کیا دیکھ سکتے ہیں

نتائج کا خاندان

متعلقہ مقالوں کا مجموعہ، جس میں معاون دلائل، نتائج یا متبادل ثبوت شامل ہو سکتے ہیں۔

مسودہ

ریاضی کی ایک انفرادی دستاویز، اپنی ماخذ فائلوں اور حوالہ جاتی معلومات کے ساتھ۔

استدلال کا خلاصہ

کسی منتخب نتیجے کے لیے ماڈل کے استدلال کا مختصر بیان۔

Lean فائل

رسمی تعریفیں، بیانات اور مجوزہ ثبوت، روابط اور ترتیبات کے ساتھ جو بتاتے ہیں کہ کیا جانچنا ہے۔

ذخیرے کی README ان زمروں کی وضاحت کرتی ہے اور خبردار کرتی ہے کہ تصدیق کا معیار یکساں نہیں۔ بعض نتائج کی Lean میں رسمی صورت نہیں، اور OpenAI کہتا ہے کہ غیر رسمی کام میں مسائل ہو سکتے ہیں۔ خود رسمی صورتوں کا کیٹلاگ دائرۂ کار کو "Partial progress" اور جائزے کی حالت کو unchecked درج کرتا ہے۔ یہ اشاعت کا metadata ہے، BIG CHANGE کے چلائے ہوئے جانچ پروگرام کا نتیجہ نہیں۔

عوامی فائلیں OpenAI اکاؤنٹ کے بغیر پڑھی جا سکتی ہیں۔ اعلان کے مطابق انہیں بنانے والا ماڈل اندرونی ہے اور OpenAI اسے جاری کرنے پر کام کر رہا ہے۔ اس لیے ان دستاویزات تک رسائی ماڈل تک رسائی ثابت نہیں کرتی۔

ثبوت پر عمل سے پہلے نسخہ متعین کریں

یہاں استعمال کیا گیا ذخیرے کا snapshot commit adc7f1241b42e322a6451854ab7e4b4c146bf78a ہے، مورخہ 6 اکتوبر 2026، 21:58:50 UTC۔ اس شناخت والے روابط اسی snapshot کو برقرار رکھتے ہیں؛ main والے روابط بدلتی ہوئی default branch کے ساتھ چلتے ہیں۔ OpenAI کی README وعدہ کرتی ہے کہ تصحیحات یا نظرثانی آنے پر سابقہ ریلیز محفوظ رہیں گی۔

اس سے شروع کریں: جائزہ, جو ریاضیاتی موضوع کے لحاظ سے خاندانوں کو گروپ کرتا ہے؛ پھر مخصوص مقالے تک پہنچنے کے لیے مسودوں کا نقشہ دیکھیں۔ اس کی ڈائریکٹری کا نام، ذخیرے کا commit اور مقالے کا دیا ہوا حوالہ محفوظ رکھیں۔ مسودے کی تاریخ اور عوامی مجموعے کی ریلیز کی تاریخ مختلف ہو سکتی ہیں۔

خاندان 003 کے ایک مقالے میں 7/8 کے دائیں جانب صفر سے پاک خطے کا دعویٰ ہے، 11/12 کے دائیں جانب خطے کے لیے متبادل ثبوت ہے، اور Landau–Siegel zeros پر ایک الگ مقالہ ہے۔ پہلے مقالے کی ڈائریکٹری پر 30 ستمبر کی تاریخ اور BibTeX حوالہ ہے۔ مخصوص مقالے کی نشان دہی ان دعوؤں میں فرق برقرار رکھتی ہے۔

اس کا Lean scope صفحہ بتاتا ہے کہ رسمی صورت کن بیانات کا احاطہ کرتی ہے، کیا خارج ہے، اور مقالے میں بعد کے اطلاقات چھوڑ دیے گئے ہیں۔ یہ زeta نتیجے، Dirichlet اور Hecke L-functions اور حقیقی zeros کے یکساں فاصلے کے لیے الگ جانچ بیانات سے جوڑتا ہے۔ ایک منتخب بیان کی جانچ اس صفحے کے ہر نکتے کی خودکار تصدیق نہیں۔

منتخب بیان سے اس کی ترتیب تک جائیں

OpenAI کی Comparator ہدایات خاندان 003 کو مثال بناتی ہیں۔ Comparator مجوزہ Lean ثبوت کو ایک متعین challenge سے ملانے کا آلہ ہے۔ مثال کی JSON ترتیب ایک قضیہ منتخب کرتی ہے: Riemann zeta function کا غیر صفر ہونا جب اس کے argument کا حقیقی حصہ 7/8 سے زیادہ ہو۔

یہ ترتیب ایک challenge module اور الگ solution module کی طرف اشارہ کرتی ہے۔ یہ معیاری axioms propext ، Quot.sound اور Classical.choice کی اجازت دیتی ہے، اور enable_nanoda کو false پر مقرر کرتی ہے۔ Nanoda ایک آزاد checker ہے جسے Comparator استعمال کر سکتا ہے؛ فراہم کردہ ترتیب اسے فعال نہیں کرتی۔

اس challenge فائل میں sorry ہے، جو نامکمل ثبوت کے لیے Lean کا placeholder ہے۔ یہاں اس کا مخصوص کردار ہے: ملانے کے لیے بیان فراہم کرنا۔ Comparator کی دستاویزات challenge میں placeholder کی اجازت دیتی ہیں اور solution میں درست ثبوت لازم کرتی ہیں۔ صرف challenge میں sorry ملنے سے یہ معلوم نہیں ہوتا کہ الگ solution کامیاب ہے یا نہیں۔ Comparator کی دستاویزات.

دستاویزی مقامی جانچ کے لیے یہ ترتیب، اس کے challenge اور solution modules اور ان کے dependencies درکار ہیں۔ ذخیرہ Lean 4.34.1کو pin کرتا ہے۔ اس کا Lake manifest dependencies کے revisions درج کرتا ہے، جن میں Mathlib کا revision d13f23b723b8a846827a245b89c10fc7d3f11612 بھی شامل ہے۔

OpenAI کہتا ہے کہ comparator ، landrun اور lean4export executable search path میں ہوں، پھر ان commands کو lean/ directory سے چلانے کی ہدایت دیتا ہے:

Terminal
lake update
lake exe cache get
lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json

یہ ناشر کی ہدایات ہیں، ہم نے یہ commands نہیں چلائیں۔ ان میں ان تین بیرونی tools کے نسخے pin نہیں۔ Comparator کی موجودہ دستاویزات مطابقت رکھنے والا lean4export درکار قرار دیتی ہیں، sandbox کی شرائط بیان کرتی ہیں، اور بتاتی ہیں کہ کامیابی کب challenge سے مطابقت، اجازت یافتہ axioms کے استعمال اور kernel کی قبولیت کی تصدیق کرتی ہے۔ قابلِ تکرار رپورٹ میں ذخیرے کے commit کے ساتھ نصب شدہ tool versions اور اصل output درج ہونا چاہیے۔

Lean library کی README اس بڑی لائبریری کے چھوٹے حصے مرتب کرنے کی تجویز دیتی ہے۔ یہ Linux میں memory mapping کی ایسی حدود بھی درج کرتی ہے جو مکمل build روک سکتی ہیں۔ ہم نے اس مثال کا مقامی runtime یا hardware cost نہیں ناپا۔

کامیاب جانچ کو اس کے بیان کردہ دائرے میں سمجھیں

Lean کا validation reference, جسے دیکھتے وقت نسخہ 4.35.0-rc3 تھا، رسمی ثبوت کی قبولیت اور قضیے کے معنی کی تشریح میں فرق کرتا ہے۔ دستاویز کا یہ نسخہ ذخیرے کے pinned toolchain سے الگ ہے۔

بنیادی جانچ کی کامیابی کا مطلب ہے کہ kernel نے تعریفوں، imports اور axioms کے تحت رسمی بیان قبول کیا۔ dependencies میں نامکمل ثبوت باقی ہو سکتے ہیں۔ Lean استعمال شدہ axioms دکھانے کے لیے #print axioms کی وضاحت کرتا ہے، جس میں dependency chain کے نامکمل ثبوت کے لیے sorryAx بھی شامل ہے۔

زیادہ مضبوط جانچ محفوظ شدہ ثبوت دوبارہ چلا سکتی ہے یا solution کا الگ سے متعین بیان سے موازنہ کر سکتی ہے۔ پھر بھی یہ جانچ کے ماحول اور مطلوبہ معنی کے درست اظہار پر منحصر ہے۔ اسی لیے verification report میں اصل challenge، اجازت یافتہ axioms اور بیرونی checker کی ترتیبات درج ہونی چاہئیں۔ نہ kernel کی قبولیت، نہ challenge سے مطابقت، journal کی منظوری یا مسودے کے ہر دعوے کی رسمی صورت ثابت کرتی ہے۔

compute کا عدد تخلیق کے عمل کو بیان کرتا ہے

OpenAI کے مطابق ہر نتیجے پر اوسطاً اتنی computing لگی جتنی ChatGPT Pro میں تقریباً تین گھنٹے سوچنے پر لگتی ہے۔ README کہتی ہے کہ evaluation میں لگ بھگ 4,000 مسائل دیے گئے، پھر outputs کو گروپ کر کے اہم نتائج چنے گئے۔ یہ معمول کے طریقے سے استثنا بھی بتاتی ہے۔ یہ کمپنی کے generation اعداد ہیں؛ ان سے قاری کی Lean جانچ کی قیمت یا کل ڈالر بل معلوم نہیں ہوتا۔ ریلیز کا اعلان, generation کی وضاحت.

خاندان 003 کے لیے یہ جائزہ zeta کا ایک مخصوص بیان، مجوزہ solution اور checker کے منظور کردہ axioms شناخت کرتا ہے۔ یہ بھی ثابت کرتا ہے کہ فراہم کردہ مثال میں Nanoda بند ہے۔ اس ترتیب کی کامیابی معلوم کرنے کے لیے اسے چلا کر نتیجہ درج کرنا ہوگا۔

ماخذ اور مزید مطالعہ

  • 6 اکتوبر کا OpenAI اعلانریلیز کی تاریخ، ماڈل کی اندرونی حالت، منصوبہ بند اضافوں اور کمپنی کے compute تخمینے کی تصدیق کرتا ہے۔ یہ developer کی اپنی کارکردگی کا بیان ہے۔
  • Pinned ذخیرہیہاں دیکھے گئے کیٹلاگ، مسودے کی فائلیں اور ثبوت کی ترتیبات فراہم کرتا ہے۔ اعداد مکمل فہرست اور مسودوں کے نقشے سے آئے؛ منتخب رسمی فائلیں چلائے بغیر پڑھی گئیں۔ ترتیب سمجھنے کے لیے جائزے کا LaTeX source دیکھا۔
  • Lean کا validation referenceثبوت کی جانچ کے معنی اور حدود واضح کرتا ہے۔ ہم نے 4.35.0-rc3 reference استعمال کیا؛ OpenAI project میں Lean 4.34.1 pin ہے۔
  • Comparator کی دستاویزاتchallenge اور solution فائلوں، ماحول کی شرائط اور مشروط ضمانتوں کی وضاحت کرتی ہیں۔ یہ اس مجموعے کے لیے verification result نہیں دیتیں۔
  • Kingy.ai پر Curtis Pyke کا جائزہریلیز کا آزاد جامد معائنہ پیش کرتا ہے۔ اس میں واضح ہے کہ آزادانہ Lean execution نہیں ہوئی؛ ہم اسے ثبوتی جانچ کی تکرار نہیں سمجھتے۔
  • AI ریاضی پر BIG CHANGE کی سابقہ رپورٹمئی تا ستمبر کی ترتیب بیان کرتی ہے۔ یہ مضمون نئے مجموعے کے artifact ڈھانچے اور معائنے کے عمل کا جائزہ لیتا ہے۔