PaperFormalizer يحوّل مقالات LaTeX إلى شيفرة Lean تم التحقق منها بمشاركة المؤلف

اقترح فريق من ستانفورد طريقة يُراد لها أن تجعل التحقق الرسمي من المقالات الرياضية جزءًا روتينيًا من إعداد النشر. أداة PaperFormalizer، التي أصدرها جيويان تان وفاسيليس سيركانيس وخوسيه بلانشيه، تحوّل المصدر البرمجي لمقالة LaTeX إلى نسخة من العمل تم التحقق منها عبر Lean. وتعمل كخط معالجة وكيلي داخل Claude Code أو Codex. والفكرة الأساسية أن المقالة، حتى لو روجعت بعناية، قد تحتوي على ثغرات صغيرة في البراهين أو في صياغة الافتراضات، وأن أفضل من يسدّها هو المؤلف نفسه، بمساعدة الآلة.

خط المعالجة من LaTeX إلى Lean

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

يستخدم خط المعالجة عدة مصادر في البراهين:

• Mathlib، المكتبة الرياضية الرئيسية في Lean؛
• مكتبات اختيارية متخصصة بمجال معيّن؛
• مجموعة أدوات شخصية للمؤلف، أي مبرهناته المساعدة وتعريفاته الخاصة.

تتراكم هذه المجموعة مع الوقت. وكلما مرّر المؤلف مقالات أكثر عبر النظام، زاد عدد اللبنات الجاهزة المتاحة للمقالة التالية.

المؤلف هو من يحدد ما تقوله المقالة

تعاني الصياغة الرسمية الآلية عادةً من استبدال صامت للمعنى. فقد يبرهن النموذج مبرهنة سليمة شكليًا تمامًا، لكنها لا تقول ما قصده المؤلف. وينطلق مطوّرو PaperFormalizer من أن المؤلف وحده يعرف ما ينبغي أن تعنيه العبارة، وأفضل طريقة لسد ثغرة الصياغة الرسمية.

لذلك يتبع النظام عدة قواعد:

• إذا احتملت العبارة أكثر من قراءة، يتوقف خط المعالجة ويطرح سؤالًا؛
• يُقدَّم كل تصحيح بلغة طبيعية وبرموز TeX بوصفه اقتراحًا يمكن قبوله أو رفضه أو إعادة توجيهه؛
• أي قرار قد يغيّر ما تعلنه المقالة يبقى بيد المؤلف.

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

ماذا يحصل عليه المؤلف في النهاية

تتكون نتيجة العمل من ثلاثة أجزاء:

• نسخة مشروحة ومصححة من المقالة؛
• تقرير بجميع التغييرات التي أُدخلت؛
• شيفرة Lean يرتبط فيها كل تصريح بالعبارة التي يصوغها رسميًا.

هذا الربط الأخير مهم للقارئ. فيمكنه فتح أي مبرهنة في النص ورؤية كائن Lean المتحقق منه المقابل لها، بدلًا من البحث عن التطابق يدويًا.

مكتبة مشتركة للأعمال المتحقق منها

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

نُشرت الأداة على GitHub في المستودع Jiyuan-Tan/PaperFormalizer. وصدر العمل في 22 أكتوبر 2026 وأُدرج في القائمة اليومية لـ Hugging Face Papers؛ وتُذكر الجهة في صفحته باسم Stanford University.

الأهمية العملية للباحثين

بالنسبة إلى الرياضيين والنظريين في الإحصاء والاقتصاد وتعلّم الآلة، ممن تقوم استنتاجاتهم على البراهين، تتيح الأداة الحصول على تحقق مستقل قبل الإرسال إلى المجلة. وتفيد بوجه خاص حيث تمرّ أخطاء الافتراضات من المراجعة دون أن يلاحظها أحد. وعتبة الدخول أدنى من الصياغة اليدوية في Lean: يلزم المصدر البرمجي لمقالة LaTeX، والوصول إلى Claude Code أو Codex، والاستعداد للإجابة عن أسئلة النظام.

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