لقد حققت النماذج اللغوية الكبيرة تقدماً ملحوظاً في إنتاج الأدلة الرياضية الدقيقة مؤخراً. في المقابل، يظل استخدام النماذج اللغوية الكبيرة في إثبات النظريات بلغات رسمية (مثل Lean) تحدياً كبيراً ومرتّباً من حيث التكلفة الحسابية، خصوصاً عند التعامل مع المسائل على مستوى البكالوريوس وما يتجاوزه. في هذا العمل، نقدّم Seed-Prover 1.5، نموذجاً لإثبات النظريات الرسمية تم تدريبه عبر تعلم التقييم الوكيل على نطاق واسع، إلى جانب تدفق عمل فعّال يُسمى التوسع في وقت الاختبار (TTS). من خلال التفاعلات الواسعة مع Lean وأدوات أخرى، يُكثّف النموذج خبرته أثناء عملية التعلم عبر التقييم (RL)، مما يُحسّن بشكل كبير القدرة والكفاءة في إثبات النظريات الرسمية. علاوةً على ذلك، وباستغلال التطورات الحديثة في إثباتات اللغة الطبيعية، يُمكّن تدفق العمل TTS من تقليل الفجوة بين اللغة الطبيعية واللغة الرسمية بشكل فعّال. مقارنةً بالأساليب المتطورة حديثاً، يُحقّق Seed-Prover 1.5 أداءً متفوّقاً بحاجة أقل إلى موارد الحوسبة. إذ نجح في حل 88% من مسائل PutnamBench (على مستوى البكالوريوس)، و80% من مسائل Fate-H (على مستوى الدراسات العليا)، و33% من مسائل Fate-X (على مستوى الدكتوراه). وبشكل ملحوظ، استطعنا، باستخدام نظامنا، حل 11 من أصل 12 مسألة من مسائل Putnam 2025 خلال 9 ساعات فقط. تشير نتائجنا إلى أن التوسع في التعلّم من الخبرة، المُحرّك بتعليقات رسمية عالية الجودة، يمتلك إمكانات هائلة لمستقبل التفكير الرياضي الرمزي.