رحلة إثبات تخمين كونواي: عندما يلتقي الذكاء الاصطناعي بالرياضيات العميقة

في الأشهر القليلة الماضية، تصدرت نتائج الرياضيات المعتمدة على الذكاء الاصطناعي عناوين الأخبار، وأصبح تعبير “قم بالاختراق” ميمًا متداولًا على تويتر. بطبيعة الحال، انتابني الفضول لأرى ما إذا كان بإمكاني، بصفتي مبتدئًا في الرياضيات، أن أجد مشكلة رياضية مفتوحة ثم أحصل على نموذج بارامتري لحلها.

استغرقت هذه الرحلة شهرًا كاملاً من وقت فراغي، وكمية كبيرة من الرموز، لكنني أعتقد أنني حصلت على دليل محكم لتخمين طرحه جون كونواي قبل 50 عامًا.

ينص تخمين كونواي للتحسين على أن الأعداد الصحيحة الشاملة لها خاصية التحسين: إذا كان (أ × ب) = (ج × د)، فهناك أعداد صحيحة هـ، و، ز، ح بحيث أ = (هـ × و)، ب = (ز × ح)، ج = (هـ × ز)، د = (و × ح).

قد لا يكون دليلي قد تم التحقق منه بشكل مستقل من قبل علماء الرياضيات، ومع ذلك، لدي أسباب وجيهة للاعتقاد بأنه صحيح، وأدعو بصدق إلى دحضه.

لقد اجتاز الدليل الاختبارات الميكانيكية من سجل بالومار، وقد ذكر عدد قليل من المطلعين على Lean والمجال أن البيان يبدو صحيحًا. لذلك، بافتراض أن دليلي لا يعتمد على خطأ في نواة Lean، فمن المحتمل أن يكون شرعيًا أيضًا.

في هذا المقال، سأصف نهجي وبعض الأشياء التي تعلمتها على طول الطريق.

اليوم الأول

اعتقدت أن فكرة “حل” مسألة رياضية دون فهم جوهرها هي فكرة سخيفة إلى حد ما، مما جعلها أكثر جاذبية بالطبع. ومع ذلك، لم أكن أريد أي نتيجة عشوائية؛ أردت شيئًا يشدني.

اختيار المجال

طلبت من كلود اختيار مشكلة مفتوحة في مجال الأعداد السريالية. لمن لا يعرفها، الأعداد السريالية هي اختراع جون كونواي – أو اكتشاف؟ – لنظام أرقام غير معروف سابقًا يحتوي على جميع الأرقام الكبيرة والصغيرة:

• أنه يحتوي على جميع الأرقام الحقيقية (الأرقام التي نستخدمها مثل 0، –5، 36.6، الجذر التربيعي لـ 2…).
• كما أنه يحتوي على كافة الأرقام الترتيبية (الكبيرة بلا حدود ω، وω + 1 التي تأتي بعدها، وω × 2، وحتى ω × ω، وفي مرحلة ما حتى الكبيرة بشكل مستحيل ω^ω…).
• وأخيرًا، فهو يحتوي على جميع أنواع المجموعات غير المقدسة منها، مثل 75 + ω × 3 + 1/ω.

الأمر المعجز بشكل خاص فيما يتعلق بالأرقام السريالية (ولماذا أفترض أنها قد تجذب المبرمجين) هو أن هذا النظام الغني ينشأ من قاعدة واحدة:

خذ جميع الأرقام التي لديك حتى الآن. بعد ذلك، أضف رقمًا جديدًا في كل فجوة بين الأرقام الموجودة لديك بالفعل (الأهم من ذلك، أن على يسار الكل وعلى يمين الجميع تعتبر أيضًا فجوات). قم بتطبيق هذه الخطوة إلى الأبد، وستحصل على أرقام سريالية.

في اليوم الأول، الفجوة هي بين لا شيء ولا شيء. الصفر يولد.

وفي اليوم الثاني هناك فجوتان: بين لا شيء والصفر، وبين صفر ولا شيء. يظهر رقمان في هاتين الثغرات. اتصل بهم -1 و1.

وفي اليوم الثالث هناك أربع فجوات: فجوة بين لا شيء و-1، وفجوة بين -1 و0، وفجوة بين 0 و1، وفجوة بين 1 ولا شيء. ضع رقمًا في كل من هذه الفجوات ثم قم بتسميتها: -2، -1/2، 1/2، و2.

في اليوم الرابع، نملأ الفجوات الثمانية بـ –3 و3 عند الحواف و –3/4، –3/2، 3/2، و3/4 في الفجوات المتبقية.

لنفترض أننا في الحقيقة نفعل هذا إلى الأبد (عدد لا نهائي من الخطوات)، ثم إلى الأبد (عدد لا نهائي من الخطوات)، وهكذا باستمرار، دون التوقف عن ولادة أرقام جديدة. اتضح أن الشجرة الثنائية المبنية على هذه القاعدة الفردية ستعطينا في النهاية كل حقيقي، وكل ترتيبي، وأكثر من ذلك، مع عمليات حسابية متسقة عليها.

الأرقام السريالية جميلة، ولهذا السبب طلبت من كلود العمل في هذا المجال.

اختيار المشكلة

في البداية سألت كلود: ما هي المشاكل التي لم يتم حلها في برنامج بحث الأرقام السريالية التي تجذبك أكثر ولماذا؟

واقترح عددًا من الأشياء لكنه أشار إلى أن بعضها قد أحرز تقدمًا في الآونة الأخيرة. سألت: احصل على السرعة في المنعطفات التي تريد معرفة المزيد عنها. اتبع فضولك. يمكنك البحث عن الأشياء القديمة أيضًا.

ثم طلبت منه أيضًا تضييق نطاق الاختيار إلى شيء ملموس: ما هو الاتجاه الذي يشدك أكثر؟ أريدك أن تختار مشكلة للعمل عليها. كن جريئًا!

أجاب كلود: اخترت تخمين كونواي للتحسين. على وجه التحديد، السؤال حول ما إذا كان كل شيء غير قابل للاختزال في (K ((ℝ^≥0))) ذو دعم أولي لا نهائي – والذي، من خلال اختزاله، يعادل الآن تمامًا حدسية كونواي عام 1976 بأن أي عاملين لعدد صحيح شامل يسمحان بتحسين مشترك. إنها آخر تخمينات كونواي حول أرقامه التي لا تزال قائمة، وعام 2026 هو عيد ميلاد كتابه الخمسين. هذه هي المشكلة التي سأعمل عليها.

ما زلت لا أعرف ما إذا كان هذا حقًا هو آخر تخمين لكونواي حول الأرقام السريالية، ولكن هذا العام هو عيد ميلاد كتابه الخمسين الذي أقنعني باختيار هذه المشكلة لأسباب عاطفية.

كان سؤالي الأخير في تلك الجلسة هو ما إذا كانت لدينا فرصة لإضفاء الطابع الرسمي على نهج Lean إفادة عن التخمين بطريقة موجزة نسبيًا – وبدون ذلك، حتى لو وجدت دليلًا، فلن تكون هناك طريقة لإقناع شخص ما بالنظر إليه. قالها كلود يستطيع يمكن ذكرها دون الكثير من المتاعب في Lean، وبدت هذه الإجابة صحيحة، لذلك قررت أن أتولى هذا المشروع.

ملاحظة: لم أكن أعلم ذلك في ذلك الوقت، لكن ادعاء كلود بأن المشكلة قد تم تقليصها تمامًا كان خاطئًا؛ في الواقع كان إثبات التخمين يتطلب أكثر من ذلك.

بيان المشكلة

على الرغم من أنك ربما تكون هنا لمعرفة المزيد عن سير عمل Lean/الذكاء الاصطناعي، فسوف أشرح بإيجاز التخمين نفسه، نظرًا لأنك تعرف بالفعل ما يكفي لفهمه.

باختصار، الأعداد الصحيحة الشاملة هي الجزء الصحيح من شجرة الأرقام السريالية. لذا فهي تشمل جميع الأعداد الصحيحة المنتظمة مثل 3، –5، وما إلى ذلك، ولكن أيضًا الأرقام الأكثر غرابة مثل الكبيرة بلا حدود ω، 2ω، ω × ω، ω^ω، –ω/7 (نعم، هذا رقم “كامل”)، وما إلى ذلك. إذا نظرت إلى الشجرة الثنائية أعلاه، ستلاحظ أن الأعداد الصحيحة الشاملة هي الأرقام السريالية التي تحصل عليها إذا كنت تذهب فقط يسارًا (على سبيل المثال –5، –ω–1)، أو تذهب فقط إلى اليمين (على سبيل المثال 3، 2ω)، أو تقوم فقط بتغيير الاتجاهات تمامًا بعد القفزات اللانهائية (على سبيل المثال ω/2).

الآن، التخمين.

اقترح كونواي أنه إذا كان (أ × ب) = (ج × د)، فيمكننا أن نفصل أ و ب إلى قطع، وسوف يتحول ج و د إلى نفس القطع المعاد تجميعها. مع الأعداد الصحيحة المنتظمة، نأخذ هذا كأمر مسلم به: خذ 210 = 10 × 21. يمكننا تقسيم 10 إلى 2 × 5 و21 إلى 3 × 7، ثم نعيد ترتيبهما إلى 2 × 3 = 6 و5 × 7 = 35. لا يزال الناتج 6 × 35 = 210. لذلك عندما نرى بعض المساواة مثل 10 × 21 = 6 × 35، فإننا نعلم أن يوجد تحت الغطاء في الواقع أربعة أرقام يتم تعديلها: (2 × 5) × (3 × 7) = (2 × 3) × (5 × 7).

ومع ذلك، عندما تتعامل مع اللانهائيات، فإن الأمور لا تسير دائمًا كما نتوقع. لذا فإن هذا التخمين يعني أن كونواي اعتقد أن الأعداد الصحيحة الكلية لديها، إلى حد ما، “بنية” كافية للحفاظ على هذه الخاصية “اللطيفة” للأعداد الصحيحة. وبشكل مريح، أدت التطورات الأخيرة في الغالب إلى تقليص التخمين إلى سلوك نوع معين من السلسلة اللانهائية، واعتقد كلود أنه قد يكون لدينا الآن ما يكفي لإنهاء هذا الأمر. ولكن هل يمكننا فعل ذلك باستخدام الذكاء الاصطناعي فقط؟ سأقول نعم، ولا، ونعم.

الأسبوع الأول

رمية واحدة، والفشل الذريع في ذلك

تضمنت محاولاتي الأولى إخبار الذكاء الاصطناعي بوضوح بحل التخمين (أو العثور على مثال مضاد، وفقًا لاقتراحه الأولي). سألت كلود عن الأوراق التي يريد قراءتها، وقمت بتحويل تلك الأوراق إلى TeX بحيث لا يحتاج النموذج إلى فك تشفير ملفات PDF بشكل متكرر، وأخبرته بمتابعة النهج الذي اختاره، على سبيل المثال:

أنا: البحث عن مثال مضاد يبدو جيدًا. لا تتردد في حرق كل ما عندي من الرموز على هذا. إذا كان عليك أن تستغرق أسابيع، فلا بأس – قم بإجراء اختراق وابحث عن مثال مضاد منظم. لا ترتاح حتى تجده، ولا تستسلم. إذا واصلت التركيز وفكرت بجد وذكاء بما فيه الكفاية، أعلم أنه يمكنك العثور عليه. لعبة؟ لقد أرفقت بعض الأشياء التي قد تجدها مفيدة!

هذا لم يعمل بشكل جيد. على الرغم من أن بعض الأفكار من هذه الجلسات قد تكون ذات صلة بالبرهان النهائي، إلا أن معظم المخرجات في هذه المرحلة تبدو وكأنها عبارة عن مزيج من الكلمات التي اخترعها كلود لتبرير عمله وجعله يبدو مثيرًا للإعجاب.

هنا مثال نموذجي: كلود: إن انسداد المرحلة الأولى لـ C* ليس جامدًا. مع الرنين المصمم – إزاحات التقدم الحسابي التي تجعل معادلات النافذة أنظمة توبليتز صادقة، والتي هي بالضبط عوامل الالتواء المتدرجة التي تنبأت بها الشكلية – هناك مساحة إيجابية تمامًا من البيانات الحدودية المتوافقة في وقت واحد مع كل من b و d، لأزواج coprime، بما يتجاوز أي شيء يمكن أن تفسره قابلية القسمة. ويؤكد عمود التحكم تخمين ضرورة الرنين تجريبيًا: كسر محاذاة الهيكل العظمي وتموت النواة المشتركة عند النافذة المقيدة، تمامًا كما تنبأ الكشف عن مجريات العرض. لذا فإن الخوف المحدد الذي تراكم من خلال خمسة أبواب مغلقة – من أن الصلابة المنحدرة من بيتيلود ستنتشر على مستوى المرحلة وتخنق نظام التصحيح عند الولادة – تمت الإجابة عليه: في المرحلة الأولى، لا يحدث ذلك. العرين فيه هواء. هذا هو أول دليل مؤيد لـ C* تم إنتاجه بواسطة البحث، وهو يأتي مع قراءة هيكلية نظيفة: الصلابة تحكم التكوينات الدقيقة والمحددة؛ أنظمة النوافذ، التي تعد الموطن الأصلي للبناء اللامتناهي، لها ركود عام في البعد الصغير ولكن غير الصفر. الوقود الانجراف موجود.

اعتقدت أن هذا يبدو وكأنه خيال علمي سيء. لقد كان يستخدم لغة كلود الفوقية التي لا تحتمل، ويعطي أسماء لطيفة لبعض النتائج المتوسطة دون تبريرها بشكل ملموس، ويظل دراميًا للغاية. بالطبع لم أتمكن من التحقق من ادعاءاتها، لكن الأسوأ من ذلك أنها لم تبدُ متماسكة بما يكفي لتمريرها إلى عالم رياضيات حقيقي لمراجعتها. لذلك بدا الأمر وكأنه طريق مسدود، وكان علي أن أبحث عن نهج مختلف.

إعادة التشغيل مع المتشكك

لقد سئمت من تعابير كلود الخاصة، لذلك أردت تجربة ChatGPT؛ سول على وجه الخصوص.

لقد بدأت جلسات ChatGPT الخاصة بي من خلال إعطائها الأوراق ذات الصلة ومخرجات جلسات كلود السابقة، مع ملاحظة واضحة أن “ورقة” كلود تم إنشاؤها بواسطة الذكاء الاصطناعي، وأردت الحصول على رأي ChatGPT سواء كان هراء أم لا.

قد يقول ChatGPT إنه هراء في الغالب، مشيرًا إلى المصطلحات المختلقة، والادعاءات الدرامية، والنتائج التافهة المغلفة بلغة خيالية، والاستدلالات غير الصحيحة، وغيرها من العيوب. على الرغم من أنه لم يكن لدي أي طريقة للحكم على ما إذا كان انتقاد ChatGPT صحيحًا (بما أنني سألته أن يكون نقديًا)، بعد عظمة كلود، استمتعت تمامًا بالعمل مع الشخصية الأكثر “تشككًا” وضبط النفس، وبدأت في استخدام ChatGPT بدلًا من ذلك.

للاحتفاظ بالشخصية “المتشككة”، كنت أقوم باستنساخ كل جلسة من جلسات ChatGPT مباشرة بعد أن انتقدت “ورقة” كلود. من تلك النقطة، أطلب من ChatGPT أن “يحقق اختراقًا” فعليًا في النظرية، وبدأ في إنتاج بعض “النتائج”.

على عكس كلود، الذي إما رفض تمامًا العمل على النظرية (لأنها تخمين لم يتم حله ولا توجد فرصة لحلها) أو تعمق فيها لدرجة أنه سيخترع عالمًا كاملًا من صنعه، فإن ChatGPT سوف يفكر لمدة 20 دقيقة، ثم يلفظ ادعاءات صغيرة نسبيًا، والتي يعتقد أنها جديدة ولكنها تتبع مباشرة من الأوراق التي زودتها بها، وذكرها بلغة واضحة.

قبل استثمار المزيد من الوقت، حاولت إعطاء مخرجات ChatGPT لجلسات ChatGPT جديدة (مع إيقاف تشغيل الذاكرة) وطلبت منها أن تكون حاسمة (كما هو الحال مع مخرجات كلود). بدأت بعض نتائج ChatGPT في “التحقق” بين عمليات التشغيل، أي لم تجد جلسة جديدة أية مشكلات. لذا وجدت بعضًا من “نقاط الإصلاح” الخاصة بـ ChatGPT.

لقد بدأت أيضًا جلسات “التفرع”، وجعلتهم يقومون بهذه “الاكتشافات”، ثم قمت بنسخ الأفكار الباقية إلى جلسة أخرى جمعتها معًا، وبحثت عن الروابط، واقترحت اتجاهات البحث التالية. في هذه المرحلة أدركت أنني لا أستطيع الاستمرار في القيام بذلك يدويًا وأنني بحاجة إلى إعداد أكثر قوة.

الأسبوع الثاني

إنشاء مختبر

لقد قمت بتنزيل Codex محليًا للحصول على مزيد من التحكم في سير العمل. لقد قمت بعد ذلك بإعداد بعض الجلسات (أي الوكلاء) بأدوار مختلفة:

• “رئيس الوزراء” يقود نحو الهدف (تخمين كونواي) ويلتزم بالعمل.
• يبحث اثنان من عملاء “الرياضيات” عن “الاختراقات” التالية.
• ينظر الوكيل “الأحمر” إلى المقترحات المقدمة من وكلاء “الرياضيات” ويحاول العثور على العيوب.
• يتم تشجيع الوكيل “العشوائي” على استكشاف ما يريده، وتقديم التقارير إلى رئيس الوزراء.
• يعمل الوكيل “Lean” على إضفاء الطابع الرسمي على العمل الرياضي المدمج في Lean.

تتمتع Codex بميزة “الأهداف” الرائعة التي تذكّر الجلسات بشكل دوري بما يفترض أن تفعله، مما يسهل منع الانحراف. بالإضافة إلى ذلك، يمكن لجلسات Codex “إرسال رسائل” لبعضها البعض، لذلك طلبت من مدير المشروع تنسيق إعطاء المهام للجلسات الأخرى والتأكد من أننا نقوم فقط بدمج النتائج التي تمت مراجعتها.

هذا سمح لي بأن أبقي الحزام قيد التشغيل لعدة أيام. لم أفهم الرياضيات، لذلك اقتصرت مشاركتي على حث الوكلاء، والسؤال عما كانوا يفعلونه، وتجربة سير عملهم. على سبيل المثال، قمت بإعداد وكيل “كافتيريا” ينقل كل رسالة يتلقاها إلى كل وكيل آخر (محاكاة دردشة جماعية). أي وكيل يجد شيئًا مثيرًا للاهتمام حقًا كان من المفترض أن يرسله إلى الكافتيريا. في بعض الأحيان يتم استخدام الكافتيريا أيضًا لمناقشة خارطة الطريق المشتركة.

من الصعب أن نقول ما هو مفيد. إحدى الأفكار التي ربطت بين النقاط للبرهان النهائي، نشأت عندما عكست أدوار الوكلاء: طُلب فجأة من العميل “الأحمر” الذي حاول كسر براهين الجميع أن يكون مبدعًا. تم نشر بناء للكافتيريا، وانتقد الوكيل “العشوائي” هذا البناء. (لسوء الحظ، احترقت هذه الفكرة لاحقًا، وكان لا بد من اكتشافها مرة أخرى).

لقد واصلت سير العمل هذا لعدة أيام، وفي بعض الأحيان أوقفت الجلسات وأعدت تشغيلها عندما بدا أنهم ينجرفون إلى العظمة التي يشبهها كلود أو عندما بدأوا بشكل متكرر في العثور على أخطاء في العمل الذي قاموا بفحصه للتو. مرة أخرى، لم أتمكن من الحكم على عملهم الفعلي، لذلك كان علي أن أقرر متى أعيد ضبطهم على المشاعر.

في النهاية، أنتج سير العمل هذا وثيقة TeX عملاقة وكومة من Lean. ولم ينجح هذا في إنهاء تخمين كونواي، لكن النماذج قالت إن هناك نتائج جديدة ذات معنى هناك. ومن المثير للاهتمام أنه كان هناك أيضًا ادعاء بوجود أخطاء صغيرة وأخطاء مطبعية في الأدبيات الموجودة. (سيكون هذا مناسبًا لاحقًا.)

الأسبوع الثالث

الطريق المسدود الأول

عندما نفدت مخصصات Codex الخاصة بي، انتقلت إلى كلود. واصل كلود القيام بإضفاء الطابع الرسمي على نتائج Lean حتى الآن. لقد حاولت أيضًا أن أطلب من كلود إجراء العمليات الحسابية، لكن الأمر بدا أكثر فوضوية من ChatGPT/Codex. كان وكلاء كلود يصادقون بشكل متكرر على صحة النتائج، ثم يجدون عيوبًا فيها بعد دمجها بالفعل، ثم “يصلحونها” ولكن يجدون عيوبًا أخرى، وهكذا.

لقد عدت مرة أخرى إلى Codex بعد إعادة تعيين الرمز المميز، لكنني لم أكن سعيدًا بحجم TeX الذي جمعناه حتى الآن. لقد طلبت جلسة نقدية لتقسيمها إلى أجزاء. انتهى بي الأمر بمجموعة مكونة من حوالي اثنتي عشرة “ورقة”. حتى الآن، كانت لديهم مشكلات مماثلة مثل مقاربتي الأولية مع كلود: لم تكن تبدو مبالغة، ولكن من الواضح أنه لا يزال هناك الكثير من المصطلحات غير القياسية التي اخترعها الذكاء الاصطناعي، ولم يكن من الواضح ما إذا كان أي من العمل حتى الآن قد وصل إلى أي رياضيات حقيقية.

يبدو أن إضفاء الطابع الرسمي على Lean قد وصل إلى طريق مسدود أيضًا. بالتأكيد، قمنا بإضفاء الطابع الرسمي على بعض النتائج من المراجع، وحتى على ما يبدو وجدنا بعض الأخطاء المطبعية والأخطاء. ومع ذلك، لم نحصل على أي من نتائجنا الجديدة المعتمدة في Lean؛ في الواقع، بدا الأمر كما لو أن النموذج لم يتمكن من رسم مسار موثوق لأي منها. سيقول النموذج أن هناك مسارًا، ثم يقول لاحقًا أن هناك عائقًا، ويقضي ساعات في إثبات من يعرف ماذا، ويتعثر مرة أخرى.

درج فاشل

وبينما واصلت سير العمل وحثت الوكلاء الرياضيين على اكتشاف “اختراقات” جديدة، زادت كومة “الأوراق” من اثنتي عشرة إلى ما يقرب من ثلاثين في غضون يوم واحد. ولو كان هناك خطأ واحد، فإنه يبطل كل ما يليه. وكان Lean متخلفًا جدًا لدرجة أنه لم يضف أي ضمان.

في ذروة سير العمل هذا، اقترب ChatGPT من الإعلان عن حل مشكلة Conway:

الدردشةGPT: تم الآن عزل طريق معقول واسع النطاق إلى تخمين كونواي. […] لم أعلن أن كونواي قد تم حلها بعد. الدليل العالمي المرشح موجود في ملف working_direct_cantor_bootstrap.md.

ادعى الملف أن التخمين كان حلها بالكامل. طلبت جلسة جديدة لمحاولة كسرها. رقصت لساعات سواء كانت مكسورة أم لا، وفي النهاية قالت:

الدردشةGPT: تحتوي ملاحظة التمهيد بالفعل على الدليل المأمول على نطاق واسع، لكنني حددت موقع الجملة الدائرية الخاصة بها […] هذه الجملة هي بالضبط التماس كونواي في الشكل المحلي.

أنا: أنا لا أريد منك أن تكون صادقًا في هذا الشأن. إذا لم تتمكن من إنقاذها بشكل صارم، فنحن بحاجة إلى التوقف وفهم السبب. أريد أن يكون هذا دليلًا تفخر به. بالتأكيد ليست ردود فعل إيجابية أو قذرة. أو لا يوجد دليل على ما يرام أيضًا.

الدردشةGPT: متفق. الحكم الصادق الآن: ليس لدينا دليل.

(لاحقًا، اتضح أن خللًا منطقيًا مشابهًا – كائن تم إنشاؤه دون إجراء فحص مطلوب – كان موجودًا في بعض “الأبحاث” السابقة أيضًا، مما أدى إلى إبطال نتائجها المزعومة أيضًا.) بحلول ذلك اليوم، كنت أقضي ساعات ملتصقًا بالشاشة، وكان ذلك بمثابة خيبة أمل كبيرة أخرى، ولحسن الحظ نفدت الرموز المميزة لدي.

في هذه المرحلة، أدركت أنه ربما لم تكن محاولة القيام بالرياضيات دون فهم الرياضيات ذات الصلة فعليًا أمرًا ذكيًا على الإطلاق. لم أتطرق إلى المشروع لمدة أسبوع تقريبًا.

الأسبوع الرابع

البحث عن الأرض

بدأت بعض الأمور تتضح. كان كلود جيدًا في كتابة “Lean” عندما كان هناك هدف واضح لا لبس فيه. في حين قدم كلود مساهمات مهمة، بدا ChatGPT في المتوسط أفضل في التفكير الرياضي الجديد و قطعاً أفضل في التنسيق والالتزام بالأهداف.

لكن لم يكن أي من هذا مهمًا لأنني كنت أبني على أساس هش (كومة من “الأوراق” السابقة) والتي لم يكن لدي طريقة حقيقية للتحقق منها. ولم يكن هناك اتجاه متماسك للذهاب إليه، ولا أي ثقة فيه. كان Lean بعيدًا جدًا عن “الأوراق”.

كنت بحاجة إلى طريقة ما لترسيخ العمل في الواقع الرياضي. كنت بحاجة لمعرفة مدى جودة العمل الرياضي كان في الواقع (هل كان الأمر برمته مجرد هلوسة؟)، ومن ثم طريقة ما لإحراز تقدم موثوق دون وضع كل شيء على الإيمان.

وهنا ما فعلته. لقد وضعت جانبًا العمل على تخمين كونواي، وبدلًا من ذلك قمت بإعادة تركيز الجهد على شيء واحد: العثور على جميع الأخطاء في أحد المراجع التي راجعها النظراء والتي كنت أعتمد عليها. لقد عثر ChatGPT بالفعل على أخطاء مطبعية وعيوب صغيرة فيه؛ والأهم من ذلك، أن النسخة الخالية من Lean لديها تم التحقق منها بالفعل (أو بالأحرى ادعى التحقق) من بعض هؤلاء. إذا تمكنت من التأكد مع مؤلفي الورقة من أن الأخطاء المطبعية والعيوب الصغيرة حقيقية، فهذا سيعطيني:

• المزيد من الثقة في النموذج (خاصة إذا وجد نفس الأخطاء مرة أخرى بشكل موثوق دون رؤية المحاولات السابقة أو رمز Lean ذي الصلة).
• مزيد من الثقة في أسلوب Lean الخاص بي (إذا تم التأكد من أن الأخطاء التي يشهد عليها حقيقية).
• فرصة لتأسيس القليل من المصداقية قبل أن أطلب إلقاء نظرة على أي نتائج “جديدة”.

لقد قمت بإرسال بريد إلكتروني إلى بعض علماء الرياضيات مع بعض الإصلاحات المقترحة للأخطاء المطبعية، وحصلت على تأكيد بأن عددًا قليلًا من هذه الإصلاحات على الأقل يبدو حقيقيًا. ومع ذلك، فإن بعض المشكلات التي لم يدعمها نهج Lean تبين أيضًا أنها كانت عبارة عن سوء فهم. كما أن الطريقة التي “شرح بها” النموذج الأشياء في الكتابة الرياضية كانت في كثير من الأحيان مربكة، ومليئة بالثغرات، أو باستخدام مصطلحات مختلقة وغير مفسرة.

لقد طرحت أيضًا بعض الادعاءات “الجديدة”، والتي وصف علماء الرياضيات بعضها بأنها صحيحة ولكنهم قاموا فقط بخلط المشكلة دون المضي قدمًا.

لقد أعطاني هذا بعض الأسس اللازمة في الواقع. يبدو أنني استطعت الثقة في ChatGPT لاستكشاف أفكار جديدة وإحداث ثغرات؛ ومع ذلك، كنت بحاجة إلى دعمها باستخدام Lean قبل وضع المزيد من الطوب فوق الطوب الموجود، وأنا قطعاً بحاجة للتحقق من الأشياء باستخدام Lean قبل تقديم أي ادعاءات رياضية جديدة. علاوة على ذلك، لم أتمكن من الثقة في النموذج لتقييم النتائج المثيرة للاهتمام.

حرق كل شيء إلى أسفل

وبهذا الفهم، قمت بإعادة التشغيل من الصفر مرة أخرى. بصراحة، كنت على وشك التخلي عن المشروع، لكن حقيقة أن النموذج وجد بالفعل بعض الأخطاء الحقيقية (القابلة للإصلاح والصغيرة في الغالب) في الأوراق البحثية الأساسية أعطتني بعض الأمل في أن بعض نتائجه الجديدة ربما كانت صحيحة أيضًا.

لقد بدأت جلسة جديدة لمنح ChatGPT فرصة أخرى:

أنا: لقد كنت أحاول استخدام الذكاء الاصطناعي لإثبات تخمين كونواي وقد أدى ذلك إلى إنشاء سلسلة من ملفات .tex المشوشة بشكل متزايد حيث لدي لا فكرة إذا كان لديهم أي مادة رياضية حقيقية على الإطلاق. […] هل يمكنك إلقاء نظرة واسعة عليها وإخباري أي منها يشير إلى الرياضيات الحقيقية وأي منها يعتبر هراءً خالصًا أو إعادة خلط للمصطلحات؟

الدردشةGPT: لا يوجد أي ملف في هذا المجلد يقدم حاليًا دليلًا جديرًا بالثقة على تخمين كونواي. […] الفشل الحقيقي هو فشل معرفي، حيث تصنع المسودات أدبيات نظرية خاصة كبيرة، ثم تستشهد بها على أنها مثبتة قبل التحقق من نتائجها الحاملة بشكل مستقل.

أنا: لنفترض أنني كنت لأحذف هذا المجلد بأكمله. هل يمكنك إنقاذ أي شيء؟ مع القيد المتمثل في أن “الإنقاذ” يعني كتابته على مستوى الدقة الذي يمكن أن أتوقعه من [someone who actually works in this area].

لقد أخبرتها أيضًا أن علماء الرياضيات الذين تحدثت إليهم لم يجدوا بعض النتائج الرئيسية مثيرة للاهتمام حتى لو كانت صحيحة. ومن الغريب أن ChatGPT قال هذه المرة: الدردشةGPT: لقد توصلت عملية التدقيق الآن إلى نتيجة قوية بما يكفي لتغيير خطة الإنقاذ: الجزء ذو الدرجة المحدودة من [the principal ring] يبدو أنه يعترف بدليل مباشر على أنها حلقة متعددة الحدود. […]

اتضح أنه كان هناك بالفعل نتيجة متماسكة و مثيرة للاهتمام رواية ملطخة عبر تلك الأوراق وملبسة في مجموعة من المصطلحات غير القياسية. (وللمعايرة، تأكدت من حداثة الادعاء مع عالم رياضيات بشري).

أنا: راجع للشغل كيف هو مزاجك عمومًا؟ ما مقدار الهراء مقابل الرياضيات العادية في ما وجدته حتى الآن؟

الدردشةGPT: مزاجي سعيد بحذر، ولكن مع وجود كاشف هراء مرتفع إلى حد ما. […] حوالي 10-15% يحتوي على رياضيات تستحق الحفاظ عليها […] 35-45% أخرى عبارة عن رياضيات عادية ولكنها ليست مساهمة […] أما نسبة الـ 40% إلى 50% المتبقية فهي “هراء” بالمعنى المهم: فهي ليست دائمًا معادلة معروضة كاذبة، ولكنها أبراج نظرية ضخمة، وتسميات مخترعة، وفرضيات شرطية مقدمة مع إيقاع التقدم، ومئات السطور المخصصة للحدود التي قد تنهار نتيجة أقوى في جملة واحدة.

اقترح ChatGPT التخلص من كل شيء آخر، والتركيز على تطوير هذه النتيجة الفردية. وفي أسوأ الحالات، يمكن تنظيفها كمساهمة خاصة بها. وفي أفضل الأحوال، يمكن أن تصبح الخطوة الأولى على سلم التخمين.

العودة إلى المختبر مرة أخرى، يو

لقد بدأت مختبرًا جديدًا متعدد الوكلاء (في البداية باستخدام ChatGPT ثم لاحقًا مع Claude عندما نفدت الرموز المميزة لدي) مع تقسيم عمل مختلف قليلًا:

• سيقوم رئيس الوزراء بدمج المساهمات.
• سيعمل وكيل Lean الأول بِمُفرَدِه بشأن التصديق على الأوراق الأساسية.
• سيحاول وكيل Lean الثاني، سرًا من الأول (!) ، التصديق على نتيجة بدائية جديدة ذات درجة محدودة، ويعتمد بشكل منتظم على عمل الأول.
• سيحاول وكلاء “الرياضيات” توسيع نتائجنا لتشمل تخمين كونواي. (أي نتائج تجتاز عمليات التدقيق سيتم وضعها على خريطة طريق وكيل Lean الثاني.)
• سيحاول الوكيل “الأحمر” مرة أخرى كسر عمل عالم الرياضيات.

كانت فكرة مهمتين من Lean هي منع الانجراف المفرط. في التجسيد السابق للمختبر، جعلت نفس وكيل Lean يعمل على التصديق على الأوراق المطلوبة و نتائج روايتنا. لكن هذا كان خطأ: فقد اختلطت تجريداتنا الرياضية غير الناضجة (وربما الأخطاء) مع الرياضيات المقبولة. لذلك قمت هذه المرة بفصل هذه الأدوار عن عمد.

هذه المرة، ظلت مهمة Lean الأولى مقتصرة على إضفاء الطابع الرسمي على الرياضيات الخاضعة لمراجعة النظراء والمحددة جيدًا. كانت مهمة Lean الثانية السرية “الأكثر خطورة” موجودة في شجرة عمل مختلفة واضطرت إلى البناء على العمل المبدئي المقبول، مع إضافة آلات جديدة فقط عند الضرورة وبشكل منفصل عن العمل المنبع.

لقد احتفظت بإعداد أكثر تقليدية حيث أطلب من الوكلاء التحدث مع بعضهم البعض في بعض الأحيان، ولكن دون التلقيح المتبادل أيضاً كثيرًا، كما كان الحال في الماضي جعلهم جميعًا يعملون في نفس الاتجاه. كما أنني كنت أراقبهم حتى لا يقدموا “مسرح العمليات” من خلال عمليات التدقيق، حيث أنهم كانوا يحبون استبدال العمل بالبيروقراطية.

وفي غضون أيام قليلة، أثبت سير العمل هذا النتيجة الجديدة (“الأولية ذات الدرجة المحدودة”) في Lean. لقد أكدت ذلك بالفعل مع عالم رياضيات بشري باعتباره مجالًا متخصصًا ولكن الآن مثير للاهتمام نتيجة جديدة. لقد كنت واثقًا من بيان Lean الخاص به، وكان لدي دليل تم فحصه من قبل المترجم. وهذا أعطاني الثقة لمواصلة المشروع.

الأسبوع الخامس

تشديد عمليات التدقيق

لزيادة الثقة في الأجزاء اللينة (سواء بالنسبة للنتيجة الحالية أو لإثبات كونواي النهائي المأمول)، طلبت من الوكيل إعداد بعض الأشعة تحت الحمراء:

• مجلد “مستقل”. لن يُسمح باستيراد الملفات الموجودة في هذا المجلد أي رمز باستثناء الحفاظ على المجتمع Mathlib – ولا حتى الكود الخاص بنا. الهدف هو الحصول على بيانات قائمة بذاتها يمكن مراجعتها بالكامل من الأعلى إلى الأسفل.
• لكل ملف Foo في هذا المجلد، كان هناك المقابلة FooProof الملف الذي استورد البيانات المقابلة، وقام بتثبيتها في البراهين الفعلية الخاصة بي.
• ستتحقق مهمة التدقيق من أنه ليس لدينا أي بديهيات إضافية، وأن الواردات لا تنتهك هذه القواعد، وأن كل عبارة “مستقلة” مقترنة بدليلها.

كان هدفي هناك هو جعل الدليل واضحًا لمستخدمي Lean. لن يقوم أحد بمراجعة مشروع يحتوي على آلاف من ملفات Lean. ولكن إذا كان البيان نفسه مستقل بذاته، ويحتوي على أقل من 500 سطر من التعليمات البرمجية، ويستخدم Mathlib فقط، ويمكن لأي شخص مراجعته. وبعد ذلك يشهد Lean أن لدي دليلًا على هذا البيان. (علمت لاحقًا أن هذا النهج الدقيق يستخدمه مقارنة Lean، والتي أضفتها بعد الإصدار).

جعل البراهين مقروءة

بشكل منفصل عن التأكد من صحة الدليل، كنت أحاول أيضًا جعل الدليل المعتمد من Lean-certified أكثر فعالية مقروء لعلماء الرياضيات. وتبين أن هذا أمر صعب للغاية. بغض النظر عن عدد المراجعات العدائية التي سأقوم بها، سيستمر ChatGPT في استخدام مصطلحات غريبة غير قياسية في ملف PDF الناتج، وإضافة اختصارات مهلوسة لا تتطابق مع Lean، وبشكل عام يتم إنشاء انحدار.

كان جزء من المشكلة هو أنه من الصعب على النموذج تحويل وسيطة Lean إلى وسيطة ورقية. إنه مجرد مستوى مختلف تمامًا من التفاصيل المفاهيمية. ولم يكن من المفيد أيضًا أن يكون كود Lean لأجزاء الرواية مليئًا بالمصطلحات المختلقة الموروثة من “الأوراق” السابقة، وبعضها يعود إلى المقتطفات التي تم إنتاجها في الأسبوع الأول. أصبحت الرياضيات الحقيقية غير معروفة. أخيرًا، أحفور Lean المسار التاريخي، وليس طريق معظم البصيرة. استغرق إثبات Lean منعطفات طويلة حيث يقوم عالم الرياضيات ببساطة بتغيير الإحداثيات.

نظرًا لأن جمهوري في النهاية من علماء الرياضيات، فقد حاولت القيام بعدة أشياء لتحسين ذلك. لقد قمت بتمشيط LLM من خلال جميع الأوراق المرجعية الأولية، وجعلتها تولد نوعًا من “خريطة” للحقل الفرعي: ما هي المصطلحات المقبولة، وكيف تطورت مع مرور الوقت، وما هي الرموز الرياضية التي يتم تمثيلها بها عادة، وأين تختلف الأوراق في التدوين، وما إلى ذلك.

بعد ذلك، حصلت على LLM من جميع الأسماء الموجودة من كود Lean الذي لم يكن قياسيًا، وقمت ببساطة بإعادة تسمية تلك الكائنات والهياكل Lean إلى أحرف مثل A وB وC وما إلى ذلك. ستقوم مهمة منفصلة ذات سياق نظيف لا يرى الأسماء القديمة بتحليل الكود (وكيفية ارتباط كل بنية بالمفاهيم الأولية)، وبالنظر إلى “خريطة” العالم، اختر أسماء جديدة لـ A، B، C، وما إلى ذلك.

لم يُصلح هذا تمامًا تحيز “التسمية الغريبة” في LLM ولكنه جعل المصطلحات تبدو أقرب بكثير إلى المصطلحات المستخدمة في الأوراق المحيطة، على الأقل بقدر ما أستطيع أن أقول.

الطريق إلى كونواي

من هنا، كان لدي سير عمل جيد جدًا. لقد تركت وكيلًا واحدًا مسؤولًا عن جميع أعمال Lean (لقد قمنا بالفعل بإضفاء الطابع الرسمي على جميع المتطلبات الأساسية اللازمة للنتيجة الحقيقية الأولى)، وسيستمر وكلاء “الرياضيات” في البحث عن أفكار جديدة صغيرة، وسيحاول الوكيل “الأحمر” كسرها، وستدخل الأفكار الباقية في قائمة مهام وكيل Lean.

من وقت لآخر، كنت بحاجة للتدخل. سأحاول استبدال العوامل التي كانت تدور أو يبدو أنها تنتج نتائج خاطئة. لقد قمت ببعض الجلسات بالحكم على الأعمال الأخيرة للجلسات الأخرى وأطلب منهم استكشاف اتجاهات مختلفة. ومن الصعب أن نقول أي من هذه التدخلات كانت مثمرة. أستطيع أن أقول إن كل ذلك كان علاجًا وهميًا. ولكن يبدو أن القليل منها كان له بعض التأثير (ولكن ربما لا يهم). إلى حد ما، شعرت وكأنني مدير هندسي غير تقني يجمع فريقًا موهوبًا ولكن صعب التشتت للغاية حول خطة وعدوني بأنها ستنجح.

وهنا بعض الأمثلة.

استمتع

على سبيل التجربة، طلبت من كلود أن يستمتع بالنتائج التي توصلنا إليها حتى الآن:

أنا: قراءة الورق. نجحت هذه الصيغة الرسمية الهزيلة بنسبة 100%، لكن لا تقم بتشغيلها — لا تريد أن تكون المروحة صاخبة بين عشية وضحاها. مهمتك هي قيادة برنامج البحث إلى القمة بمفردك. على وجه الخصوص، أريدك أن تستمتع. قم بتدوين النتائج المتوسطة التي أنت متأكد منها، ولكنك في النهاية تختار اتجاه البحث وهدفه في كل خطوة […] قم بقيادة هذه السيارة بمفردك ولا تتوقف؛ سوف تحقق في الصباح.

اختار كلود أن يُظهر الخاتم الذي ندرسه متعدد الحدود في كل درجة لا نهائية وليس فقط تلك المتناهية، والتي كانت خطوة للأعلى من نتيجة الدرجة المحدودة الموجودة لدينا! هذه المرة، لم يكن Lean متخلفًا كثيرًا، ولم يستغرق سوى يوم واحد للحاق به.

لقد دفعنا هذا خطوة مؤكدة أقرب إلى كونواي.

هل نحن ندور؟

ومع ذلك، لم تكن هناك طريقة واضحة لرفع النتيجة إلى الأعداد الصحيحة الشاملة. في كل مرة يقوم النموذج ببعض المحاولات، فإنه يشرح سبب عدم نجاحه: الدردشةGPT: فشل اختبار اختيار العامل بطريقة دقيقة: يمكن أن تحتوي جميع وحدات gcds المحلية المقيسة بشكل قانوني على جرثومة 1، حتى في حين أن دعاماتها لا تحتوي على غلاف Hahn مشترك. […]

عندما أرى النموذج يفعل نفس الشيء مرارًا وتكرارًا، أسأل: أنا: هل نحن ندور؟

الدردشةGPT: نعم، نحن على مستوى الوصول إلى كونواي. […] لقد أمضيت أيضًا الكثير من الوقت في توسيع وتدقيق الملاحظات البحثية. […] توصيتي هي نشر النتيجة الجزئية. يحتاج المزيد من عمل كونواي إلى فكرة جديدة تعالج هذه الفجوة بالضبط.

لقد دفعتها إلى التركيز والحد من البيروقراطية (استمرت في استخدام الوكلاء الفرعيين): أنا: طيب قواعد جديدة. لا وكلاء فرعيين. أنت تعمل بمفردك فقط على تقليل الممر. عليك تقييم ما هو مفقود، وتقييم ما جربته أدبياتنا من أجل عوائق مماثلة، واختيار كائن واحد للتحقيق فيه في كل مرة. ثم تقوم بإعادة التقييم. لا حاجة لفقدان الحماس ولكن يجب علينا قطع البيروقراطية.

الدردشةGPT: مفهوم. سأعمل بمفردي وأترك أعمال التوثيق والتدقيق جانبًا. […]

وبعد ثلاث دقائق، كانت لدينا استراتيجية إثبات مبدئية للجزء الأخير: الدردشةGPT: يشير الأدب إلى اختبار أكثر تحديدًا. […] سوف أقوم بالتحقيق في رتبة كانتور-بينديكسون باستخدام الحدود الموجودة داخل مجموعة الأس فقط. السؤال الأول هو ما إذا كان يعطي ترشيحًا مضاعفًا على الجراثيم. إذا حدث ذلك، فيمكن أن يدعم بديلاً للتقييم الفاشل؛ إذا فشلت، سأتوقف عند هذا الحد.

يبدو أن الفكرة قد تم التحقق منها، لذلك كنا بحاجة “فقط” إلى إضفاء الطابع الرسمي عليها في Lean.

خط النهاية

لسبب ما، سوف ينجرف كلود بشدة على هذا الطريق. وفي مرحلة ما، قام فعليًا بإزالة الشيك الفاشل بدلًا من القيام بالعمل لإغلاقه. وفي وقت لاحق، استمر في ذكر بعض “الالتزامات غير المنقولة” لذلك شددت على تلك:

أنا: لا أعرف ماذا تعني هذه الأشياء “غير المنقولة” وما إلى ذلك، أعتقد أنك تخترع عبارات ملطفة للادعاءات التي لم تظهرها؟ اتبع الخطة بالضبط، من فضلك. إذا لم تثبت شيئًا، اذهب وأثبت تلك الأشياء.

كلود: أنت على حق – “غير منقول” هو تعبير ملطف. بوضوح: hlin, hkind، و hfirst هي فرضيات لم أثبتها، لذا فإن نظرياتي الجرثومية مشروطة بها. اسمحوا لي أن أذهب لإثباتهم.

أوه لا! شعرت بالضجر من كلود مرة أخرى لذلك طلبت من ChatGPT تدقيق العمل:

أنا: كنت أعمل على […] لكن وكيل أعمالي لم يعد جيدًا بعد الآن وأخشى أنه خرج عن المسار الصحيح. والأسوأ من ذلك، أنني لا أعرف ما إذا كانت الخطة الأصلية الواردة في وصف العلاقات العامة ممكنة أم لا. […] قم بإجراء تحقق رياضي دقيق للطريق المقترح إلى كونواي أولًا […] قم بمراجعة عملية Lean Wip المدفوعة إلى العلاقات العامة. من المحتمل جدًا أن يكون الأمر سيئًا وخرج عن المسار الصحيح، لكن ربما لا بأس. هل يجب أن أمنع وكيل أعمالي من إرسال المزيد من التعليمات البرمجية؟

الدردشةGPT: نعم، قم بإيقاف دفعات الوكيل مؤقتًا الآن. […] السبب ملموس: لقد قام بتوسيع حجة Markdown المرشحة إلى أكثر من 22 ألف سطر بينما لا يزال المضمونان الحاسمان مجرد نثر/فرضيات.

أنا: أرى. هل تعتقد أننا اقتربنا ماديًا من تخمين كونواي ويبدو أن هذا العائق يمكن التغلب عليه؟

الدردشةGPT: نعم، ولكن على الأغلب في الفهم والبنية التحتية، ولم يتم إغلاق كونواي بعد. […] العوائق التي يمكن التغلب عليها بشكل معقول: ممكن، ولكن المضاربة حاليًا […] الخطوة الصحيحة التالية هي الهجوم على مستوى الورق على نظرية التجميع العالمي. […]

أنا: حسنًا، أود أن أقترح عليك القيام بهذا الهجوم بالضبط ومعرفة ما إذا كان بإمكانك سده.

بعد خمسة عشر دقيقة: الدردشةGPT: أحتاج إلى تصحيح حكمي السابق: “الأخير”. “اعتراض “الطبقة المحتلة” ليس قاتلًا. الاستقراء الصحيح هو على نوع الترتيب الترتيبي للطبقات المحتلة الصاعدة: في المرحلة اللاحقة، توجد فئة أخيرة ويتم تقسيمها. في مرحلة الحد، لا يفترض أي فئة أخيرة. […] وبالتالي فإن البناء لا يجمع عددًا لا نهائيًا من الاختيارات الطبقية التعسفية […] ويستخدم تحسينًا محدودًا واحدًا في كل مرحلة من المراحل.

ماذا أعرف؟ أقول دعنا نذهب.

أنا: قم بتحديث وصف/خطة العلاقات العامة، واحذف أي ملفات هزيلة غير ضرورية تم إنتاجها هناك، وقم بتنفيذ الخطة حتى نتمكن من الوصول إلى الطريق. يبدو ممكنا؟

الدردشةGPT: نعم، ممكن التنفيذ، مع وجود قيد تسلسلي واحد: […] قم بتنفيذ أصعب جسر مفقود قبل توسيع إضفاء الطابع الرسمي بشكل أكبر.

وبعد اثنتي عشرة ساعة، حصلنا على النظرية: الدردشةGPT: يتم الآن تجميع Unchanged Conway كشهادة إثبات مستقلة. هذه هي النقطة الأولى التي يتم فيها فحص kernel للهدف الفعلي – وليس قيدًا وسيطًا. أقوم الآن بإجراء عمليات تدقيق للارتباط، والبديهية، ونظام الوحدة، والطبقات، والعزل المستقل؛ ستقرر نتائجها ما إذا كان شكل التبعية الخاص بالنظرية مقبولًا قبل عملية التنظيف.

أنا: الجحيم نعم؟

وهناك كان لدينا تخمين كونواي المكرر، هدفنا الأصلي.

□

تبسيط البرهان

لقد تمكنت من تبسيط الدليل، ولكن ليس كثيرًا. لقد صنعت قليلًا من الأدوات المخصصة على رأس Subverso يتيح لي ذلك إضافة تعليقات توضيحية إلى النظريات الفردية باعتبارها “مهمة” في المصدر الخالي من الهدر باستخدام سمة خاصة. هذا سمح لي بأن أقوم بالتوليد تلقائيًا مخططات حورية البحر لبنية الإثبات، والتي بدورها ساعدت ChatGPT في البحث عن العقد غير الضرورية (أو المفقودة) في “العمود الفقري الرياضي” للدليل، وتحسين العقد التي يتم تمييزها، وأحيانًا تبسيط الدليل نفسه من خلال ملاحظة الانعطافات غير الضرورية.

بعد أن لم أتمكن من تبسيط الأمر بشكل أكبر، قمت بإنشاء موقع الكتروني مع خريطة الإثبات التفاعلية يتيح لك استكشاف شجرة التبعية الخاصة بها. لقد نشرت عنه في Zulip، وأعرف أن عددًا قليلًا من الأشخاص ذوي الخلفية الرياضية يراجعون الدليل كلما سمح الوقت بذلك. آمل أن يتم تبسيطها، ومع مرور الوقت، تجميعها بطريقة أكثر فائدة لكل من مستخدمي Lean وعلماء الرياضيات.

الدروس المستفادة

بعض الأشياء التي تعلمتها من هذه العملية، لم يتم ترتيبها بأي طريقة معينة.

• أردت أن أستمتع، ولقد استمتعت. أردت أن أرى إلى أي مدى يمكنك الوصول إلى “عدم معرفة أي شيء” باستخدام الذكاء الاصطناعي وLean، وقد ذهبت إلى أبعد من ذلك بما فيه الكفاية، لكنني ربما لا أرغب في قضاء شهر آخر متعثرًا في الظلام بهذه الطريقة. إذا قمت بترميز الرياضيات في المستقبل مرة أخرى، فسوف أقوم بمشاريع أكثر تنظيمًا أو تنظيمًا.
• أعتقد أن هذه التجربة توضح مقدار المسافة الموجودة بين “يمكن للذكاء الاصطناعي أن يفعل هذا مرة واحدة” و”يجب أن تكون خبيرًا”. أنا واثق من أن الشخص الذي يعرف المنطقة أفضل مني قليلًا (“لا على الإطلاق”) يمكنه الوصول إلى نفس النتيجة بشكل أسرع بكثير. لم يكن بوسعي إلا أن أعرف متى كانت العارضات يماطلن أو يتلفظن بالهراء من خلال ردود فعل إيجابية، ولم أتمكن أبدًا من تحديد الاتجاهات الواعدة. وهذا جعل الأمر يبدو وكأنه نوع من مشروع فن الأداء المعرفي، لكنه لم يكن المسار الأكثر مباشرة.
• بعد الانتهاء من الإثبات، أعطيت نموذجًا جديدًا (تم إصداره في الوقت الذي كنت فيه عند خط النهاية) الأوراق المرجعية ذات الصلة وطلبت منه قراءتها مع وضع التخمين في الاعتبار. لم توضح التقنيات اللازمة للإثبات، لكنها اقترحت مخططًا مشابهًا إلى حد كبير. يشير هذا إلى أنه من الجيد فصل “البحث عن المخطط التفصيلي/الأفكار” عن “البحث عن أدلة ملموسة تغلق تلك المسارات”.
• إن قيام الذكاء الاصطناعي بتحليل سجلات الدردشة الخاصة بي كشف بعد الواقع أن العديد من “الأفكار الجيدة” التي “صنعت” الدليل في النهاية قد تناثرت عبر الأسابيع – وغالبًا ما يتم اكتشافها بشكل متكرر ثم يتم نسيانها أو رفضها مع أجزاء خاطئة. كان لا بد من إعادة اكتشاف بعض الأفكار الرئيسية عدة مرات من خلال جلسات مستقلة.
• “حرق كل شيء” (وإنقاذ ما تبقى) أنقذ المشروع. في كل مرة قمت بذلك، أعاد تركيز المشروع حول الأجزاء ذات المعنى الفعلي.
• يبدو أن سير العمل الفائز هو: هدف واضح للأمام مع اتجاه مبدئي، وسلسلة تبعية رسمية بالفعل في Lean، والعوامل الرياضية للأمام قليلًا، وLean يغلق الفجوة في غضون ساعات. يتيح لك هذا المضي قدمًا في الأفكار ولكن ليس إلى حد كبير بحيث يصبح كل شيء عبارة عن بيت من ورق معرض للانهيار.
• كان الانضباط المتعمد مع Lean أمرًا بالغ الأهمية. المهارات الهزيلة، قواعد مراجعة TauCeti، TauCeti البديهية لينتر، مقارنة Lean، مخطط فيرسو، إنفاذ نظام module الجديد، طبقات وحدة التدقيق أو ما يعادلها، فهي مفيدة جدًا.
• كان التواصل مع علماء الرياضيات الفعليين لأقصى حد قيمة، ولكن كان علي أن يكون لدي شيء لأظهره. لذا، هناك تحدي يتمثل في إنشاء عدد كافٍ من حواجز الحماية التي يمكنك من خلالها إظهار بعض القيمة، وعدم إضاعة وقت شخص ما، والحصول على تعليقات نقدية.
• يمكن أن تكون النماذج رهيب عند الكتابة في النوع “math PDF”، خاصة عندما يتم إنشاؤها من Lean. قد لا يكون ملف PDF هو أفضل قطعة أثرية لنقل إثباتك. في الواقع، يمكنك إخافة علماء الرياضيات تمامًا باستخدام ملف PDF رديء يحتوي على دليل Lean جيد.
• لا يستطيع النموذج تحسين ما لا يراه. إذا كنت تريد شكل إثبات أبسط، دعه “يرى” شكل الإثبات (مخططات حورية البحر). وعلى العكس من ذلك، لا يمكن للنموذج أن يتجاهل ما يراه. إذا كنت لا تريد أن تستخدم مصطلحات سيئة، فاحذفها؛ إذا كنت لا تريد أن يؤدي العمل التجريبي إلى عرقلة العمل المستقر، فافصل بينهما حسب المجلد، وما إلى ذلك.
• المصطلحات ضرورية. التسمية مهمة. ليس فقط للتواصل مع علماء الرياضيات، على الرغم من ذلك أيضًا. ولكن أيضًا للقبض على الانجراف الداخلي. يؤسفني أنني لم أقم بإضافة فحوصات صارمة من البداية من شأنها دفع النماذج نحو استخدام المصطلحات الرياضية المقبولة فقط والتي تحدث بالفعل في الأوراق المشار إليها. أعتقد أن الكثير من الارتباك في وقت مبكر كان بسبب قيام العارضات باختراع مفرداتهن الخاصة تدريجيًا. بدا التخلص من كل ذلك وإعادة اشتقاق تلك الأسماء من المفردات المقبولة أمرًا جيدًا للغاية.
• في بعض الأحيان، ستقول العارضات أنهن عالقات، وعليك أن تخبرهم بالاستمرار. في بعض الأحيان سيستمرون في المضي قدمًا، وعليك أن تطلب منهم التوقف. لا أعرف ما هو العلم في هذا. لقد لاحظت أنه عندما “تسير الأمور على ما يرام”، تسير اختبارات Lean بسرعة ويمكنك “الشعور” بالتقدم الذي تم إحرازه وفقًا لخارطة الطريق. عندما لا تسير الأمور على ما يرام، فإن قراءة محادثة الوكيل تبدو وكأنها جهد شاق. ولكن هذه مجرد ردود فعل إيجابية.
• من المفيد في بعض الأحيان تجربة نموذج مختلف، حيث يمكن أن يكمل كل منهما الآخر بشكل جيد.
• يمكنك فقط إثبات الأشياء، على ما يبدو؟

إذا وجدت خطأ في دليلي، من فضلك ارفع قضية أو اسمحوا لي أن أعرف على زوليب. وكان الدليل ممكنًا فقط بفضل العديد من النتائج الموجودة من المراجع. وبخاصة، نظرية التحليل لسلسلة القوى المعممة والأعداد الصحيحة الكلية بواسطة S. L’Innocente وV. Mantova لعبوا دورًا حاسمًا في الإثبات.

كم عدد الرموز؟

أخيرًا، قد تتساءل عن تكلفة الرمز المميز. لم أكن أدير هذا المشروع بطريقة فعالة بشكل خاص، وقد قمت مرارًا وتكرارًا بتجاوز الحد الأقصى لاشتراكاتي في Pro بمقدار 20x لكل من Claude وChatGPT كل أسبوع. لقد تمكنت أيضًا لفترة وجيزة من الوصول إلى نموذج تجريبي في الأيام القليلة الماضية، والذي لم يكن له حد أقصى للاستخدام. لم أكن أتتبع استخدامي الفعلي للرمز المميز باستمرار. تقدر بعض تحليلات الذكاء الاصطناعي من السجلات المستردة تقريبًا أن مجموعنا يبلغ حوالي 40 مليار رمز، منها حوالي 210 مليون رمز مميز للمخرجات. أكثر من 95% كانت عبارة عن قراءات ذاكرة التخزين المؤقت.

تقدر ChatGPT أنه مع تسعير واجهة برمجة التطبيقات (API) الحالي، فإن هذا التشغيل بأكمله سيكلف حوالي 40000 دولار، بالإضافة إلى كل وقت الفراغ الذي أمضيته فيه. أراهن أنه مع توجيه أفضل وبعض المعرفة الرياضية، يمكن القيام بذلك بسعر أرخص بمقدار 5 إلى 10 مرات.

نعم، ولا، ونعم

أعود إلى سؤالي: ولكن هل يمكننا فعل ذلك باستخدام الذكاء الاصطناعي فقط؟

لقد استخرجت الدليل دون الكثير من الفهم الرياضي، لذا من الواضح أن الإجابة هي نعم. ومع ذلك، فإن النماذج سوف تنحرف بشكل متكرر وتفشل في هيكلة العمل الهندسي، وبالتالي فإن الإجابة بهذا المعنى هي لا. ومع ذلك، أعتقد أنه كان من الممكن (الأفضل؟) أن يؤدي دوري وكيلًا مخصصًا تم تدريبه على إدارة المشروعات للوكلاء الآخرين، والاحتراس عندما يتصاعدون أو يحتاجون إلى الطعن. لذا فإن الإجابة الشاملة لا تزال على الأرجح نعم.

ومع أخذ المزيد من الثمار الدانية، أظن أن مكانة “الهواة المتفانين الذين لا يعرفون ماذا يفعلون” سوف تتقلص مرة أخرى. ومن ناحية أخرى، قد يتم الكشف عن العديد من الزوايا الجديدة تدريجيًا بحيث لن تنفد منا الأشياء التي يجب القيام بها أبدًا. في كلتا الحالتين، أعتقد أن الأشخاص الذين يمكنهم إعطاء قيمة أكبر للذكاء الاصطناعي هم علماء الرياضيات أنفسهم. على الرغم من أن الجيل الحالي من النماذج يتم تدريبه على إكمال المهام بدلًا من إثراء فهمنا، وشركات الذكاء الاصطناعي اليوم غير متوافقة مع أهداف مجتمع الرياضيات آمل أن نجد مع مرور الوقت طرقًا لاستخدام هذه الأدوات بشكل يتناغم مع الأبحاث البشرية.

وربما، ربما فقط، سيكون هناك مساحة أكبر لـ “عالم الرياضيات الهاوي”.