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