
قال تشارلز هوسكينسون، مؤسس كاردانو، في 9 سبتمبر إن الذكاء الاصطناعي قد أحرز تقدمًا في الرياضيات الشكلية يفوق توقعاته.
جاءت تعليقاته عقب ادعاء OpenAI بأن نظامًا داخليًا أنتج حلاً لمشكلة نافييه-ستوكس لجائزة الألفية.
خلال بث مباشر، وصف هوسكينسون القدرات المبلغ عنها بأنها "مميزة للغاية". ومع ذلك، تطرق أيضًا إلى الأسئلة غير المحسومة حول مصدر العمل وخصوصية الأبحاث المقدمة لخدمات الذكاء الاصطناعي القائمة على السحابة.
قال هوسكينسون إنه كان يتوقع في الأصل أن تساعد الأنظمة الشكلية فرقًا أكبر من علماء الرياضيات على التعاون والتحقق من البراهين المكتوبة من قبل البشر. لم يكن يتوقع أن تقوم نماذج اللغة الكبيرة بتوليد براهين كاملة بنفسها بهذه السرعة.
قال هوسكينسون: "لم نتوقع أبدًا المدى الذي سيصل إليه الذكاء الاصطناعي". وأضاف أن فكرة قيام الذكاء الاصطناعي بكتابة برهان كامل كانت تبدو في السابق "بعيدة جدًا".
لدى هوسكينسون علاقة مباشرة بأبحاث الرياضيات الشكلية. في عام 2021، تبرع بمبلغ 20 مليون دولار لجامعة كارنيجي ميلون لإنشاء مركز هوسكينسون للرياضيات الشكلية، وفقًا لإعلان الجامعة.
تتوافق تعليقاته الأخيرة أيضًا مع تجارب كاردانو الأوسع مع الذكاء الاصطناعي. كما أفادت crypto.news سابقًا، دافع هوسكينسون عن تجارب وكلاء الذكاء الاصطناعي في كاردانو التي تشمل الاتصالات ونشاط المجتمع ونظام Midnight البيئي الذي يركز على الخصوصية.
نشرت OpenAI بحثها في 8 سبتمبر. وقالت الشركة إن نموذجًا داخليًا نسق حوالي 10,000 وكيل وأنتج حلاً مقترحًا بعد 88 ساعة. ثم أمضى GPT-6 Astra 17 ساعة إضافية في صياغة الحجة والتحقق منها في Lean.
يحاول البرهان إثبات أن سائلًا أملسًا وساكنًا في البداية يمكن أن يطور تفردًا في وقت محدود عند تعرضه لقوة خارجية ناعمة. قالت OpenAI إن هذا يفي بالبيانين C و D في صياغة جائزة الألفية الرسمية.
أصدرت الشركة أيضًا ورقة تحليلية وكود Lean. يوفر التنسيق الرسمي في Lean تحققًا يمكن فحصه آليًا بأن الخطوات المشفرة تتبع الافتراضات المذكورة. لكنه لا يثبت بشكل مستقل أن كل تعريف وافتراض يمثل بدقة المشكلة الرياضية المقصودة.
قالت OpenAI إنها لا تخطط للسعي للحصول على الجائزة المرتبطة التي تبلغ مليون دولار. ومع ذلك، وصفت الشركة عملها بأنه حل للمشكلة.
لا يزال معهد كلاي للرياضيات يصنف مشكلة نافييه-ستوكس بأنها "غير محلولة". لم يعترف موقعه الإلكتروني بالبرهان المقترح من OpenAI كحل مقبول وقت إعداد التقرير.
لا يقبل معهد كلاي الحلول المقترحة من خلال التقديمات المباشرة. بموجب قواعده، يجب أن يظهر الحل في منشور مؤهل. ثم يجب أن تمر سنتان على الأقل، ويجب أن يحظى العمل بقبول عام من مجتمع الرياضيات العالمي.
تعني هذه العملية أن إعلان OpenAI وإثباتها الرسمي لا يشكلان اعترافًا مؤسسيًا فوريًا. يجب على علماء الرياضيات فحص ما إذا كان البناء يفي بالصياغة الدقيقة للمشكلة وما إذا كان استخدامه للقوة الخارجية يجيب على السؤال كما هو مفهوم بشكل شائع.
أثار الإعلان أيضًا تدقيقًا شمل عالم الرياضيات تريستان باكماستر من جامعة نيويورك والباحث ليفنت ألبوجي من Anthropic. كان الباحثان يعملان على نتيجة معادلة أويلر ذات الصلة باستخدام نهج القوة.
تساءل باكماستر عما إذا كانت الأعمال الخاصة المدخلة في نظام Codex الخاص بـ OpenAI قد تكون قد ساهمت في نتيجة الشركة. لم يتهم بسوء سلوك مثبت، قائلاً: "لا أعرف ما إذا كانت بياناتنا قد استخدمت".
نفت OpenAI الوصول إلى عملهم المحدد. ومع ذلك، قالت الشركة إنها لا تستطيع استبعاد احتمال أن تكون البيانات مجهولة الهوية من استخدامهم للمنتج قد ساعدت في تحسين نماذجها. أكدت OpenAI أن برهانها تم تطويره بشكل مستقل ويختلف عن عمل الباحثين.
جادل هوسكينسون بأن النزاع يجب أن يثير قلق الباحثين الذين يتعاملون مع الأفكار غير المنشورة. وقال إن الباحثين الذين يستخدمون خدمات الذكاء الاصطناعي المركزية يجب أن يأخذوا في الاعتبار ما إذا كانت الأوامر والملاحظات وسجلات البحث تظل سرية.
ستتضمن المرحلة التالية فحصًا عامًا لورقة OpenAI والتنسيق الرسمي في Lean. حتى يقوم المتخصصون بمراجعة الافتراضات وتلبية الشروط الرسمية لمعهد كلاي، يظل العمل حلاً مزعومًا وليس حلاً معترفًا به.





