نُقدّم إجراءً تدريبيًا آنيًا (Online Training) لمعالج رياضي تلقائي يعتمد على نموذج المحولات (Transformer-based Automated Theorem Prover). يعتمد نهجنا على خوارزمية بحث جديدة تُسمى بحث البرهان الشجري الفائق (HyperTree Proof Search - HTPS)، والتي استلهمت من النجاح الأخير لنموذج AlphaZero. يتعلم نموذجنا من عمليات البرهان السابقة من خلال التدريب الآني، مما يمكّنه من التعميم على مجالات بعيدة جدًا عن التوزيع التدريبي. ونُقدّم تحليلًا مفصّلًا لمكونات خط أنابيبنا الرئيسية من خلال دراسة الأداء في ثلاثة بيئات تتزايد تعقيدها تدريجيًا. وبشكل خاص، نُظهر أن نموذجًا مدربًا على براهين مُعلّمة، عند استخدامه مع HTPS فقط، يتمكن من إثبات 65.4% من مجموعة مُتَوَقّفة من نظريات Metamath، متفوّقًا بشكل ملحوظ على الحالة السابقة من الأداء التي بلغت 56.5% باستخدام GPT-f. كما أن التدريب الآني على هذه النظريات غير المُثبتة يرفع الدقة إلى 82.6%. وبمجرد استخدام ميزانية حسابية مشابهة، نُحسّن الحالة الحالية من الأداء على مجموعة بيانات miniF2F-التي تُبنى على Lean من 31% إلى 42% من دقة إثبات النظريات.