1215 ورقة بحثية
تقدم هذه الورقة منطقاً من الدرجة الأولى موجهاً يتميز بالمساواة غير المتماثلة ونظاماً تركيبياً قائماً على القطبية، موفرةً دلالات فئوية سليمة وكاملة عبر "عقائد موجهة" (directed doctrines) تُعرف المساواة الموجهة بوصفها مرافقاً أيسر نسبياً وتعمم مساواة لافير الكلاسيكية.
تقدم هذه الورقة خوارزميات لتحديد وحساب جميع الأصفار الـ -adic لمتتاليات التراجع الخطي، والتي تُعد صحيحة دون قيد وتتوقف تحت فرضية "شانويل" للـ -adic، مما يُمكّن من تقرير قابلية القرار لمسألة "سكولم" المتزامنة للمتتاليات المتباينة تحت نفس الفرضية.
تقدم هذه الورقة خريطة اقتران حقنية، خالية من الحمل، من إلى تقوم بتشفير رقمين في نطاقات مؤشر "زيكندورف" منفصلة يفصل بينهما فاصل، مما يتيح التقييم والعكس من خلال عمليات الدعم الجمعي دون ضرب أو تحليل إلى عوامل، مع التحقق من صحة الجوهر في Rocq.
تقدم هذه الورقة إجراء توحيد سليم وكامل للأنماط محددة الحتمية التي تعمم الأساليب الحالية من خلال تخفيف قيود وسيط المتغير، رغم أن هذا التقدم يؤدي إلى مجموعات قد تكون لانهائية من الموحدات ويترك قابلية التقرير للمسألة كقضية مفتوحة.
مدفوعاً بالتحليل الحسابي، تدرس هذه الورقة النقاط الثابتة للمتداخلات متعددة الحدود الليفية لتطوير بناء نحوي لتعبيرات التي تلتقط درجات "ويراوخ" ذات المعنى، والتي تتراوح من الاختيار المغلق إلى حتمية لعبة التكافؤ اللانهائية، وذلك من خلال تفسير الجبرات الأولية، والكو-جبرات النهائية، ونقطة ثابتة مبتكرة في فئات الحاويات.
تقدم هذه الورقة MathlibLemma، وهو مسار مؤتمت يعتمد على النماذج اللغوية الكبيرة لاكتشاف وصياغة لِمات "الفلكلور" المفقودة لتوسيع مكتبة Lean Mathlib، مع إنشاء معيار شامل يتضمن أكثر من 4,000 عبارة رياضية مُحققة للنهوض بالرياضيات المساعدة للذكاء الاصطناعي.
تقدم هذه الورقة إطار عمل جديد لترميز نموذج إيسينج/QUBO يستخدم تمثيل ثنائي القطبية لدمج دلالات "عدم الاهتمام"، مما يتيح الحساب الفعال للتعيينات الجزئية المرضية القصيرة (المُستنتجات) وتقليلها من خلال استرجاع الحالة الأرضية.
تقدم هذه الورقة دلالات شريط تتبع الأدلة للحوسبة الاحتمالية التي توحد المنظورين المفهومي والامتدادي من خلال إطار عمل قابل للتحقق، مما يتيح منطقاً من الرتب العليا مع محولات أدلة موحدة لاستنباط قوانين كمية سليمة ودعم الاستدلال باحتمالية واحد عبر تجريدات إعادة توصيل الشريط والدفع الأمامي.
تقترح هذه الورقة دلالات فئوية للمنطق الخطي التفاضلي عبر نمذجته كزوج من رتيبات غروتينديك (Grothendieck fibrations) المزودة بدالة مماسية، وذلك عبر تكييف طرق نظرية الأنواع مع ثنائية الخطية-غير الخطية كخطوة تأسيسية نحو توحيد المنطق الخطي التفاضلي مع الأنواع التابعة.
تقدم هذه الورقة معياراً مضبوطاً يوضح أن تعزيز وكلاء البرمجة بالذكاء الاصطناł عبر نظام استرجاع سياق المنتج (Brief) يحسن امتثالهم للقرارات الخاصة بالمنتج والخاصة بالفريق بمقدار 49 نقطة مئوية مقارنة بالوصول إلى الكود المصدري فقط، محققاً نسبة امتثال تصل إلى 95% في مهام هندسة البرمجيات الواقعية.