في إثبات النظرية، يُعد اختيار الفرضيات المفيدة من مكتبة كبيرة لفتح طريق إثبات افتراض معين أمرًا بالغ الأهمية. ويُشكل هذا تحديًا كبيرًا لجميع مُثبتات النظرية، وخاصة تلك القائمة على نماذج اللغة، نظرًا لضعف قدرتها النسبية على التفكير في كميات هائلة من الفرضيات المكتوبة بالنص. يقدّم هذا البحث إطار عمل يُدعى Thor، يدمج بين نماذج اللغة ومُثبتات النظرية التلقائية لتجاوز هذه الصعوبة. في إطار Thor، تُستخدم فئة من الأساليب تُسمى "الهُمّات" (hammers)، التي تستفيد من قوة مُثبتات النظرية التلقائية في اختيار الفرضيات، بينما تُسنَد جميع المهام الأخرى إلى نماذج اللغة. يرفع إطار Thor معدل نجاح نموذج اللغة على مجموعة بيانات PISA من 39% إلى 57%، ويحل 8.2% من المسائل التي لم تتمكن نماذج اللغة أو مُثبتات النظرية التلقائية من حلها بشكل منفصل. علاوةً على ذلك، وبمجرد ميزانية حوسبة أصغر بشكل ملحوظ، يمكن لـ Thor تحقيق معدل نجاح على مجموعة بيانات MiniF2F يوازي أفضل الأساليب الحالية. ويمكن تطبيق إطار Thor على معظم مُثبتات النظرية التفاعلية الشائعة من خلال بروتوكول بسيط نقدّمه.