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