ترجمة البيانات الرياضية المكتوبة بلغة الطبيعية إلى شفرة قابلة للتنفيذ رسمياً هي تحدي أساسي في إثبات النظريات الآلي. بينما ركزت الدراسات السابقة على نجاح التوليد والتقفيل، فقد تم تجاهل مرحلة النقد - وهي تقييم ما إذا كانت الصياغات الرسمية المُنتجة قد أدركت بالفعل النوايا الدلالية للمشكلة الأصلية. في هذا البحث، نقدم "CriticLean"، إطار جديد للتعلم التعزيزي بقيادة النقد يرفع من دور الناقد من مدقق سلبي إلى مكون تعليمي فعال. بشكل خاص، نقترح أولاً "CriticLeanGPT" (مُدرب عبر التحسين الإشرافي والتعلم التعزيزي) لتقييم دقة المعنى في صياغات Lean 4 بشكل دقيق. ثم، نقدم "CriticLeanBench"، معيارًا مصممًا لقياس قدرة النماذج على التمييز بين الصياغات الرسمية الصحيحة والخاطئة دلالياً، ونوضح أن نماذج "CriticLeanGPT" المدربة لدينا يمكنها أن تتخطى بكفاءة كبيرة القواعد الأولية القوية ذات المصدر المفتوح والمغلق. اعتماداً على إطار "CriticLean"، نقوم ببناء "FineLeanCorpus"، وهو مجموعة بيانات تتضمن أكثر من 285 ألف مشكلة تتميز بتعدد مجالاتها وتنوع صعوبتها وصحتها العالية بناءً على تقييم البشر. بشكل عام، تؤكد نتائجنا أن تحسين مرحلة النقد ضروري لإنتاج صياغات رسمية موثوقة، ونأمل أن توفر "CriticLean" رؤى قيمة للتقدم المستقبلي في الاستدلال الرياضي الرسمي.