أقترح نظامًا للبرهنة الآلية على النظريات في المنطق من الرتبة العليا باستخدام التعلم العميق وتجنب الخصائص المبنية يدويًا. يستغل نظام هولوفرازم (Holophrasm) الصيغة الرسمية للغة ميتاماث (Metamath) ويستكشف أشجار البراهين الجزئية باستخدام خوارزمية بنديت مدعمة بالشبكات العصبية ونموذج تحويل التسلسلات لعد الأفعال. يثبت النظام 14% من نظرياته الاختبارية من وحدة set.mm في ميتاماث.