# Axiom تحوّل مشروع Stacks إلى شيفرة Lean مدقّقة آليًا

> تقول Axiom إن تحويل مرجع بارز في الهندسة الجبرية إلى 16 مليون سطر يتيح إعادة استخدامه في براهين يتحقق منها Lean.

Oossa · 2026-11-05 · https://oossa.com/ar/axiom-turns-the-stacks-project-into-machine-checked-lean-code

أصدرت Axiom Math نسخة مدقّقة آليًا من مشروع Stacks، وهو مرجع مهم مفتوح المصدر في الهندسة الجبرية. ويحوّل هذا العمل رياضيات المشروع إلى نحو 16 مليون سطر من شيفرة Lean، يفحصها برنامج للتحقق من البراهين خطوةً خطوة. وتقول Axiom إن الباحثين ووكلاء الذكاء الاصطناعي يستطيعون استخدام هذه النتائج بوصفها مكتبة مترابطة عند بناء براهين رسمية جديدة.

تورد المصادر أعدادًا مختلفة قليلًا للصفحات: إذ تشير TechCrunch إلى نحو 7,654 صفحة، فيما تصف Axiom المشروع بأنه يضم قرابة 7,500 صفحة. وبدأ عالم الرياضيات في جامعة كولومبيا يوهان دي يونغ إعداد المرجع الأصلي عام 2005، ثم أسهم رياضيون في توسيعه على مدى عقدين. ويحوّل عمل Axiom هذا النتاج العلمي القائم إلى صيغة رسمية؛ ولا يعني ذلك أن وكلاء الذكاء الاصطناعي اكتشفوا الرياضيات التي يستند إليها بصورة مستقلة.

## لماذا تكتسب المكتبة المترابطة أهمية؟

لا تقتصر فائدة مكتبة البراهين على التحقق من مبرهناتها كلٌّ على حدة؛ إذ يمكن للبراهين اللاحقة إعادة استخدامها والاستناد إلى تبعياتها. وتقول Axiom إنها حافظت على الوسوم الدائمة في مشروع Stacks، وربطت تعريفات Lean بالأجزاء المقابلة لها في النص الأصلي. كما يتيح موقع الشركة عرض النص إلى جانب الشيفرة واستكشاف اعتماد النتائج بعضها على بعض.

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

## أساس لبراهين وبرمجيات مستقبلية

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

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

## الحقائق

- أعلنت Axiom إصدارها في November 4, 2026.
- تتضمن الصيغة الرسمية بـLean نحو 16 مليون سطر من الشيفرة.
- بدأ يوهان دي يونغ إعداد مشروع Stacks عام 2005، ونما المشروع بمساهمات من رياضيين.
- جمعت Axiom مبلغ $200 million في جولة Series A قادتها Menlo Ventures في March 2026، بحسب TechCrunch.

## لماذا يهم

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

## المصادر والمراجع

1. [Axiom Math wants to keep AI slop out of mathematics](https://techcrunch.com/2026/11/05/axiom-math-wants-to-keep-ai-slop-out-of-mathematics/) – TechCrunch, 2026-11-05
2. [Axiom](https://axiommath.ai/research/the-stacks-project-formalized/?utm_source=openai) – Axiom

آخر تحديث: 2026-11-05