في عالم الرياضيات المعقد، تسعى الأبحاث الحديثة إلى تجاوز العقبات التقليدية التي تواجه تحليل الأعداد. في الآونة الأخيرة، أثبتت الجهود الأخيرة أن الوكلاء البرمجيون (coding agents) قادرون على تحويل كتب الرياضيات المتقدمة بكامل محتواها إلى لغة رسمية باستخدام Lean 4. ومع ذلك، فإن معظم هذه الجهود تركز على فروع الرياضيات التي تم تمثيلها بشكل جيد في مكتبة الرياضيات (mathlib)، وتقيّم النجاح استنادًا فقط إلى قبول النواة (kernel acceptance).

مع ذلك، يأتي هذا البحث ليعالج هاتين المسألتين من خلال تطبيق وكيل برمجي على كتاب "الطرق العددية للمعادلات التفاضلية العادية" (Numerical Methods for Ordinary Differential Equations)، وهو كتاب في تحليل الأعداد يفتقر إلى التمثيل في mathlib. يظهر هذا البحث قدرة الوكيل على تطوير نظريات جديدة من الصفر، مما يفتح أبواباً جديدة للابتكار.

بالإضافة إلى ذلك، يقدم الباحثون إطارًا منهجيًا ثلاثي الأبعاد لتقييم جودة التحويلات التي ينتجها الوكلاء، متجاوزين بذلك نقاط الضعف المرتبطة بالقياسات التقليدية. يتضمن هذا الإطار تقييم "الصحة الدلالية" (semantic correctness) وإعادة استخدام مكتبة الرياضيات (Mathlib reuse) وإعادة الاستخدام العابر للملفات (cross-file reuse) باستخدام الأساليب التي تعتمد على نماذج اللغات الضخمة (LLM-as-judge methods).

من خلال تطبيق هذا الإطار على عملية تحويلهم الخاصة وعلى المخرجات المنشورة من RepoProver وM2F، تم كشف النقاب عن أنماط متكررة من التحويل غير الدقيق، مثل التصريحات غير المكتملة، والافتراضات المضافة، والقيود على المعلمات، التي تغفلها معايير قبول النواة.

تشير النتائج إلى أن مقاييس التحويل المعتمدة على التراخيص قد تبالغ بشكل كبير في تقدير جودة التحويل، مما يستدعي الحاجة إلى منهجية تدقيق قابلة للتكرار لدعم تقييم أكثر دقة للأنظمة المستقبلية للتحويل الآلي. في النهاية، يمكن أن يمثل هذا العمل الجديد طفرة في مجال البرمجة وتحليل الأعداد، مما يساهم في تحسين جودة علم الرياضيات المعاصر.