1215 ورقة بحثية
تقدم هذه الورقة صياغة خالية من البديهيات في لغة Lean 4 لجوارات المنحنيات التوافقية لمتعددات فلوج الأفينية من النوع عبر ترميزها من خلال نظام كوكسيتر لمجموعة دييدرال اللانهائية، مما يوفر في النهاية إطاراً موثقاً وقابلاً للحوسبة بالكامل لهذه الجوارات.
تناقش هذه الورقة التحقق الرسمي الناجح لحل مارينا فيازوفسكا لعام 2016 لمسألة تعبئة الكرات في ثمانية أبعاد باستخدام مثبت النظريات "Lean"، مع تسليط الضوء على علامة فارقة تعاونية بين علماء الرياضيات البشر ونموذج الأتمتة الصورية "Gauss".
تعمل هذه الورقة على تحسين حدود تعقيد الوصول لأنظمة إضافة المتجهات (VAS) ذات الأبعاد الثابتة من خلال تقديم تحليل مضخة مكرر ينتج حداً علوياً ويثبت حدود PSPACE وELEMENTARY لأنظمة VAS رباعية الأبعاد وخماسية الأبعاد، على التوالي، متجاوزةً بذلك النتائج السابقة الموروثة من أنظمة إضافة المتجهات مع الحالات (VASS).
تقدم الورقة البحثية ZFLean، وهي مكتبة لغة Lean 4 تدمج نظرية المجموعات ZFC الأساسية في منظومة Mathlib مع تحسين سهولة الاستخدام، والإنشاءات المعيارية، والجسور للأنواع الأصلية لتسهيل البراهث المختلطة بين مستوى المجموعات والمستويات النوعية.
تقدم هذه الورقة أول استقصاء منهجي في التعقيد النظري لـ "أوتوماتا هانوي أوميجا" (HOA) و"ألعاب هانوي أوميجا" (HOG) التي تم صياغتها حديثاً، حيث تثبت أن ترميزها الرمزي عبر حواجز الانتقال البوليانية يرفع معضلات القرار القياسية مثل عدم الفراغ واحتواء اللغة إلى مستويات NP-complete و PSPACE/EXPSPACE-complete على التوالي، مع اشتقاق حدود تعقيد وثيقة لحل الألعاب تحت شروط قبول متنوعة.
تحلل هذه الورقة حدود أدوات تخليق البراهين الآلية الحالية، وتحدد أن أنماط التكتيكات الشبيهة بالبشر ضرورية للنجاح، وتقترح طريقة البحث عن التكتيكات الموجهة بالأنماط (PGTS) التي تحسن بشكل كبير معدلات الإثبات وإيجاز النصوص للمثبتات النظرية التفاعلية.
تثبت هذه الورقة أن الشبكات العصبية المتكررة، والمعادلات التفاضلية العادية متعددة الحدود، والخرائط متعددة الحدود، هي جميعها أطر عمل متكافئة لحساب الدوال العودية الأولية، مما يكشف كيف يعوض كل نظام منها عن القيود الهيكلية للأنظمة الأخرى — مثل التفرع، أو التقريب، أو التجزئة — من خلال خصائصه الديناميكية المحددة.
تقدم هذه الورقة خوارزمية CEGIW، وهي خوارزمية موجهة بالعديد من الأمثلة المضادة تعمل تلقائياً وبشكل أمثل على إضعاف الفترات الزمنية في مواصفات المنطق الزمني المتري لاستعادة صلاحيتها للأنظمة التي تعاني من تدهور الأداء مع الحفاظ على هيكلها المنطقي الأصلي.
تقترح هذه الورقة **NeSyCat**، وهو إطار فئوي يستخدم المونادات لتوحيد الدلالات الكلاسيكية والضبابية والاحتمالية المتباينة للغة ULLER العصبية الرمزية في نظام معياري واحد يسمح بالتوسع السهل والترجمة بين النماذج الدلالية المختلفة.
تقدم هذه الورقة نظام IBV، وهو نسخة حدسية من منطق BV، حيث توفر نظام استدلال استنتاجي مع حذف القطع، وتثبت أن متغيره غير التجميعي يشكل نسخة حدسية جديدة من منطق NML (المسمى INML) مع حساب تسلسلي خالٍ من القطع.