02:10
وفقا ل Xin Zhiyuan ، اكتشف Tao Zhexuan ، إله الرياضيات الذي يحرص على استخدام GPT-4 و Copilot لإجراء الأبحاث مؤخرا ، خطأ مخفيا في ورقته بمساعدة الذكاء الاصطناعي. هتف بعض عشاق الرياضيات في هذا المنشور: هذا مذهل ، ومن الرائع أن نرى انتشار مساعدي إثبات الذكاء الاصطناعي ، مما يضع أساسا أقوى لمستقبل أبحاث الرياضيات. قال تاو تشيشوان ، "هذا ممكن تماما. ربما في المستقبل القريب ، يمكننا بناء طبقة الذكاء الاصطناعي فوق Lean. من خلال وصف الخطوات في الدليل على الذكاء الاصطناعي ، يمكن ل الذكاء الاصطناعي استخدام Lean لتنفيذ الإثبات ، واستدعاء حزمة جبر الكمبيوتر في هذه العملية. في يونيو من هذا العام ، توقع Tao Zhexuan في مدونة حول تجربة GPT-4 أنه في عام 2026 ، سيتم دمج الذكاء الاصطناعي مع أدوات البحث والرياضيات الرمزية لتصبح مؤلفا مشاركا موثوقا به في البحث الرياضي. خلال هذه الفترة ، كان هناك أشخاص أثبتوا ذلك ، مثل علماء من معهد كاليفورنيا للتكنولوجيا ، NVIDIA ، معهد ماساتشوستس للتكنولوجيا ، ومؤسسات أخرى ، قاموا ببناء بروفير نظرية يعتمد على LLMs مفتوحة المصدر.