في عالم الرياضيات، تُعتبر الترجمة من اللغة الطبيعية (Natural Language) إلى لغات رسمية مثل Lean خطوة ضرورية للتحقق من صحة البرهانات. ومع ذلك، قد تكون عمليات الترجمة التي يتم تنفيذها بواسطة أنظمة الذكاء الاصطناعي، مثل تلك التي أطلقتها OpenAI، غير موثوقة. على الرغم من أن ترجمة البرهانات الرياضية تسهل عملية التحقق الآلي، فإن هذه الترجمة ليست خالية من المخاوف.

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

كما أظهرت النتائج أن صعوبة تحقيق الترجمة الدقيقة تعلو كل القضايا الحسابية بما فيها مشكلة التوقف (Halting Problem). فعلى سبيل المثال، تم تقديم عدة حالات من الترجمة غير الدقيقة من AI، حيث لم تتطابق الترجمة الرسمية مع البرهانات الأصلية، حتى في حالة البرهان الذي أعلنته OpenAI عن معادلات نافييه-ستوكس.

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