رياضي – إثبات رسمي وبحث في الذكاء الاصطناعي (عقد عمل عن بُعد)

نظرة عامة على الدور

رياضي – إثبات رسمي وبحث في الذكاء الاصطناعي (عقد عمل عن بُعد). ماذا لو كانت معرفتك العميقة بالرياضيات الرسمية تُشكّل مباشرةً كيفية تفكير أكثر أنظمة الذكاء الاصطناعي تطورًا في العالم وإثباتها واستدلالها؟ هذه الفرصة موجّهة لعلماء الرياضيات الشغوفين بالبرهان الصارم والأنظمة الرسمية للمساعدة في بناء الأسس الرياضية التي يعتمد عليها الذكاء الاصطناعي الحدودي

ما ستقوم به

• بناء براهين رسمية نظيفة وقابلة للقراءة ومنظّمة تُحوّل الاستدلال الرياضي غير الرسمي إلى صيغة دقيقة قابلة للتحقق آليًا
• تدقيق البراهين الرسمية الموجودة والتحقق من صحتها واكتمالها وسلامتها المنطقية
• القدرة على ترجمة الأفكار الرياضية غير الرسمية بسلاسة إلى براهين منظّمة قابلة للتحقق آليًا

المتطلبات والشروط

• الموقع: عن بُعد
• الالتزام: 10–40 ساعة/أسبوع
• الحصول على درجة الماجستير أو الدكتوراه في الرياضيات أو مجال وثيق الصلة
• امتلاك خبرة عملية مع مساعدات الإثبات الرسمي — يُفضَّل Lean 4 بشدة
• القدرة على ترجمة الأفكار الرياضية غير الرسمية بسلاسة إلى براهين منظّمة قابلة للتحقق آليًا
• الدافعية الذاتية والراحة في العمل بشكل مستقل في بيئة عمل عن بُعد وغير متزامنة
• خبرة سابقة في التحقق من البراهين أو إثبات المبرهنات أو مشاريع الصياغة الرياضية
• خبرة عبر مجالات رياضية متعددة — الطوبولوجيا والجبر والتحليل والمنطق وما وراءها

تفاصيل إضافية

• صياغة حجج رياضية متقدمة ومبرهنات في Lean 4، تغطي مجموعة واسعة من التخصصات الرياضية
• المساهمة في نمو وجودة المكتبات الرياضية الرسمية واسعة النطاق، بما فيها mathlib
• العمل في طليعة أبحاث الذكاء الاصطناعي، والمساعدة في تدريب الجيل القادم من نماذج اللغة القادرة رياضيًا