أظهرت النماذج اللغوية الكبيرة (LLMs) قدرات قوية في التفكير الرياضي من خلال الاستفادة من التعلم المعزز مع سلسلة طويلة من التفكير (long chain-of-thought)، ومع ذلك تظل تواجه صعوبات في إثبات النظريات بسبب غياب إشارات إشراف واضحة عند الاعتماد فقط على اللغة الطبيعية. تقدم اللغات المحددة للمجالات مثل Lean إشارات إشراف واضحة من خلال التحقق الرمزي من الأدلة، مما يمكّن من التدريب الفعّال باستخدام التعلم المعزز. في هذه الدراسة، نقترح نموذج Seed-Prover، وهو نموذج يعتمد على نمط البرهان الكامل بأسلوب المبرهنة (lemma-style). يتمكن Seed-Prover من تحسين إثباته بشكل تكراري بناءً على ملاحظات Lean، والنتائج المثبتة سابقًا، والتلخيص الذاتي. ولحل المشكلات التي تُطرح في المسابقات من مستوى IMO، قمنا بتصميم ثلاث استراتيجيات للاستنتاج أثناء الاختبار، تتيح التفكير العميق والواسع في آنٍ واحد. وقد تمكّن Seed-Prover من إثبات 78.1٪ من مسائل IMO الرسمية السابقة، وحقق تعبئة كاملة (saturate) لاختبار MiniF2F، وحقق أكثر من 50٪ في PutnamBench، متفوّقًا بفارق كبير على أحدث النماذج السابقة. وللتغلب على نقص الدعم الهندسي في Lean، قمنا بتطوير محرك استدلال هندسي جديد يُدعى Seed-Geometry، والذي يتفوّق على المحركات الرمزية السابقة في الهندسة. استخدمنا النظامين معًا في مسابقة IMO 2025، وتمكّنا من إثبات جميع المسائل الستة باستثناء واحدة فقط. تمثل هذه الدراسة تقدّمًا كبيرًا في مجال الاستدلال الرياضي الآلي، وتوحي بفعالية استخدام التحقق الرمزي مع التفكير الطويل المتسلسل (long chain-of-thought).