💻 computer science

ZFLean: a framework for set-level mathematics in Lean

تقدم الورقة البحثية ZFLean، وهي مكتبة لغة Lean 4 تدمج نظرية المجموعات ZFC الأساسية في منظومة Mathlib مع تحسين سهولة الاستخدام، والإنشاءات المعيارية، والجسور للأنواع الأصلية لتسهيل البراهث المختلطة بين مستوى المجموعات والمستويات النوعية.

المؤلفون الأصليون: Vincent Trélat

نُشر 2026-04-28

📖 4 دقيقة قراءة☕ قراءة في استراحة قهوة

CC BY 4.0

المؤلفون الأصليون: Vincent Trélat

البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل

تخيل أنك تحاول بناء منزل. لديك مجموعتان مختلفتان من المخططات والأدوات:

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

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

الحل: ZFLean
قام فينستنت تريلات بإنشاء ZFLean، وهو بمثابة مترجم عالمي ومجموعة من الأدوات المخصصة داخل ورشة عمل الروبوتات مباشرة.

إليك كيف يعمل، باستخدام تشبيهات بسيطة:

1. ورشة عمل "الطين" (نموذج ZFC)

يقوم ZFLean بإنشاء منطقة خاصة داخل ورشة عمل الروبوتات حيث تُطبق قواعد "الطين". هنا، يمكنك تعريف المجموعات، والعلاقات، والدوال تمامًا كما يفعل عالم الرياضيات التقليدي، دون القلق بشأن "الأنواع" الصارمة التي يطلبها الروبوت عادةً. إنها مساحة آمنة حيث يمكنك القول: "هذه مجموعة من الأعداد"، دون أن يسألك الروبوت: "هل هي من نوع Nat أم Int؟"

2. "المترجم الذكي" (الحساب العلاقاتي)

كانت أكبر مشكلة في الأيام الخوالي هي "الأعمال الروتينية" (boilerplate) — وهي الأوراق المتكررة والمملة المطلوبة لإثبات أن أشكال الطين الخاصة بك صالحة بالفعل.

الطريقة القديمة: كان عليك إثبات "نعم، هذه العلاقة هي دالة"، و"نعم، هذا المجال صالح"، يدويًا لكل خطوة.
طريقة ZFLean: يأتي الإطار مع مساعدين صغار أذكياء (تسمى التكتيكات مثل zrel و zpfun و zfun). فكر فيهم كمساعدين لملء الاستمارات تلقائيًا. عندما تكتب برهانًا، يقوم هؤلاء المساعدون تلقائيًا بفحص التفاصيل المملة وملء الأوراق نيابة عنك. أنت تكتب الرياضيات؛ والمساعدون يتولون العبء الإداري.

3. "الجسر" (التشغيل البيني)

هذا هو الجزء السحري. عادةً، كان عالم "الطين" وعالم "الروبوت" منفصلين. يقوم ZFLean ببناء جسور بينهما.

إذا بنيت مجموعة من الأعداد الطبيعية في عالم الطين، يمكن لـ ZFLean أن يقول فورًا: "مهلاً، هذا في الواقع هو النوع Nat الخاص بالروبوت".
هذا يعني أنه يمكنك القيام بـ رياضيات نظرية المجموعات الفوضوية والمرنة الخاصة بك، ثم عبور الجسر بسلاسة لاستخدام أدوات الروبوت القوية والمعدة مسبقًا (مثل حلالات الجبر) لإتمام المهمة. لا يتعين عليك الاختيار بين أحدهما أو الآخر؛ يمكنك استخدام كليهما في نفس البرهان.

4. "مجموعة الليغو" (البناءات القانونية)

لجعل الحياة أسهل، يأتي ZFLean مع مجموعة جاهزة من قطع الليغو القياسية.

هل تحتاج إلى مجموعة من قيم (صح/خطأ)؟ إليك مجموعة Boolean.
هل تحتاج إلى مجموعة من أعداد العد؟ إليك مجموعة Natural Number.
هل تحتاج إلى طريقة للتعامل مع قيم "ربما" (مثل الخيار/Option)؟ إليك مجموعة Option.
هذه ليست مجرد طين خام؛ إنها قطع مشكلة مسبقًا، ومختبرة، وتأتي مع تعليمات حول كيفية استخدامها (مثل "كيفية جمع رقمين" أو "كيفية قلب مفتاح").

5. "تجربة القيادة" (دراسة الحالة)

لإثبات أن هذا النظام يعمل، اختبر المؤلف نظامًا باستخدام لغز رياضي كلاسيكي يسمى Currying Isomorphism.

تخيل هذا: لديك آلة تأخذ مدخلين في وقت واحد (مثل صانع الساندوتش الذي يأخذ الخبز واللحم). "Currying" هي عملية تحويل هذه الآلة إلى آلة تأخذ مدخلًا واحدًا (الخبز) ثم تعطيك آلة جديدة تأخذ المدخل الثاني (اللحم).
استخدم المؤلف ZFLean لإثبات أن هاتين الطريقتين في التفكير في الآلة هما في الواقع الشيء نفسه. بدا نص البرهان مشابهًا تقريبًا لما يكتبه عالم رياضيات بشري على السبورة، مع قيام "المساعدين الأذكياء" بهدوء بمعالجة جميع المشكلات التقنية في الخلفية.

الخلاصة

ZFLean هو إطار عمل يسمح لعلماء الرياضيات بالعمل بأسلوب نظرية المجموعات التقليدية المرن والبديهي (الـ "طين") بينما يعيشون داخل نظام إثبات حاسوبي حديث وصارم (الـ "روبوتات"). إنه يزيل الاحتكاك الناتج عن الترجمة، ويؤتمت الأعمال الورقية المملة، ويبني جسورًا بحيث يمكنك استخدام أفضل الأدوات من كلا العالمين دون أن تظل عالقًا في المنتصف.

النتيجة هي مكتبة مكونة من حوالي 8,300 سطر من الكود تجعل القيام بالرياضيات على مستوى "المجموعات" في نظام Lean يبدو طبيعيًا وسلسًا مثل الكتابة على الورق.

إليك ملخص تقني مفصل لورقة البحث "ZFLean: إطار عمل للرياضيات على مستوى المجموعات في Lean" بقلم فينسنت تريلات.

1. بيان المشكلة

تعتمد الصياغة الحديثة في مساعدات الإثبات مثل Lean بشكل أساسي على نظرية الأنواع (تحديداً نظرية الأنواع المعتمدة)، حيث تُبنى الكائنات الرياضية كأنواع (types). ورغم قوة هذا النهج، إلا أنه قد يكون مرهقاً بالنسبة لـ الرياضيات على مستوى المجموعات (ZFC)، والتي يُفضلها الباحثون من أجل:

الاستدلال الامتدادي (Extensional reasoning): الاستدلال حول المساواة بناءً على العناصر بدلاً من البناء.
الجزئية (Partiality): التعامل مع الدوال الجزئية بشكل طبيعي عبر العلاقات بدلاً من ترميزها باستخدام أنواع Option أو الأنواع المعتمدة.
الاستدلال بأسلوب الفئات (Category-style reasoning): العمل "حتى التماثل" (up to isomorphism) بدلاً من المساواة التعريفية الصارمة.

التحدي: العمل مباشرة في نموذج نظري للمجموعات داخل مساعد نوعي (مثل نموذج ZFC في Mathlib الخاص بـ Lean) يسبب احتكاكاً كبيراً:

العمل الروتيني (Boilerplate): يتعين على المستخدمين باستمرار إدارة "الشروط الجانبية" (على سبيل المثال، إثبات أن العلاقة معرفة جيداً، أو إثبات أن الدالة شاملة) يدوياً.
الهشاشة (Brittleness): عبور الحدود بين كائنات نظرية المجموعات (ZFSet) وأنواع Lean الأصلية (Type) عملية يدوية وعرضة للخطأ.
نقص الأتمتة: تفتقر الأدوات الحالية غالباً إلى تلميحات إعادة الكتابة (rewriting hints) والتاكتيكات (tactics) المحددة اللازمة لجعل البراهث المعتمدة على المجموعات بسلاسة البراهث المعتمدة على الأنواع.

2. المنهجية

يقدم المؤلف ZFLean، وهو مكتبة لـ Lean 4 مبنية فوق نموذج ZFC الموجود في Mathlib. تركز المنهجية على إنشاء حساب علاقات موحد وجسور توافقية لجعل التطوير على مستوى المجموعات مريحاً وسهلاً.

خيارات التصميم الأساسية:

الأساس: يستفيد من تنفيذ Mathlib لنظرية ZFC، والتي تبني المجموعات كناتج قسم امتدادي لـ "المجموعات الأولية" (pre-sets) الاستقرائية (PSet).
الحساب العلاقي: بدلاً من معاملة الدوال ككائنات كلية أولية (كما في نظرية الأنواع القياسية)، يعامل ZFLean الدوال كـ علاقات وظيفية. إنه يقدم حسابات للعلاقات الثنائية، والدوال الجزئية، والدوال الكلية.
الأتمتة عبر التاكتيكات (Tactics): يقدم الإطار ثلاثة تاكتيكات خفيفة الوزن (zrel و zpfun و zfun) مصممة لتفريغ شروط الصحة الجانبية تلقائياً (مثل إثبات أن التركيب هو علاقة أو دالة).
الجسور: تبني المكتبة تماثلات صريحة (isomorphisms) بين كائنات ZFC المعيارية (مثل ZFBool و ZFNat) وأنواع Lean الأصلية (مثل Bool و Nat)، مما يسمح بنقل الخصائص بين العالمين.

3. المساهمات الرئيسية

أ. الحساب العلاقي والأتمتة

التعريفات: صياغة معكوس (converse)، والهوية (identity)، والتركيب (composition)، والمجال (domain)، والمدى (range)، والصورة (image) للعلاقات.
الوظيفية (Functionality): التمييز بين الدوال الجزئية (IsPFunc) والدوال الكلية (IsFunc).
التاكتيكات:
- zrel: لتفريغ الأهداف التي تثبت أن مجموعة ما هي علاقة ( $R \subseteq A \times B$ ).
- zpfun: لتفريغ الأهداف التي تثبت أن مجموعة ما هي دالة جزئية.
- zfun: لتفريغ الأهداف التي تثبت أن مجموعة ما هي دالة كلية.
- تستخدم هذه التاكتيكات ليمات (lemmas) موسومة بالسمات (مثل @[zfun]) لحل الشروط الجانبية بشكل متكرر، مما يخفي العمل الروتيني عن المستخدم.
الترميز (Notation): تقديم صيغة مريحة لتطبيق الدوال (@zf(x)) والاختزال $\lambda$ (lambda abstraction)، مع نظريات لـ $\beta$ -reduction و $\eta$ -expansion والامتداد (extensionality).

ب. البناءات المعيارية

توفر المكتبة مجموعة من الكائنات الرياضية القياسية المعرفة داخل ZFC، كاملة مع خصائصها العالمية:

القيم المنطقية (Booleans): مجموعة مكونة من عنصرين $B$ مع بنية جبرية (الوصل، الفصل، النفي) ومعامل استبعاد الحالة.
الأعداد الطبيعية ( $\mathbb{N}$ ): مُعرفة كأصغر مجموعة استقرائية (ترتيبات فون نيومان). تتضمن مسترجع (recursor)، ومبدأ الاستقراء، والعمليات الحسابية. والأهم من ذلك، أنها مجهزة ببنية CommSemiring للاستفادة من تاكتيك ring الخاص بـ Lean.
الأعداد الصحيحة ( $\mathbb{Z}$ ) والنسبية ( $\mathbb{Q}$ ): مبنية كأنواع قسم (quotient types) لأزواج من الأعداد الطبيعية/الصحيحة، مع رفع العمليات من الممثلين.
النواتج (Coproducts) والخيارات (Options): تعريفات نظرية المجموعات لأنواع الجمع (sum types) وأنواع الخيارات (option types).

ج. التماثلات والنقل

التضمينات والتماثلات: تعريف التضمينات على مستوى المجموعات ( $A \hookrightarrow_z B$ ) والتماثلات ( $A \cong_z B$ ) عبر دوال متباينة وتقابلية.
مبرهنة كانتور-شرودر-برنستين: تمت صياغتها داخل الإطار.
النقل (Transport): إثبات أن بناءات ZFC متماثلة مع أنواع Lean الأصلية (على سبيل المثال، ZFBool $\simeq$ Bool). وهذا يسمح للمستخدمين بـ "نقل" النظريات من مكتبة Mathlib الغنية بنظرية الأنواع إلى السياق النظري للمجموعات بسلاسة.

د. دراسة حالة: تماثل التقييس (Currying Isomorphism)

توضح الورقة فائدة الإطار من خلال إثبات تماثل التقييس: $C^{A \times B} \cong (C^B)^A$ .

يحدد البرهان curryz و uncurryz كدوال على مستوى المجموعات.
يثبت أنهما معكوسان متبادلان باستخدام أتمتة الإطار للتعامل مع الشروط الجانبية (صحة تعريف الدوال والتركيبات والصور).
يماثل نص البرهان الحجج الرياضية القياسية، حيث تتولى طبقة الأتمتة التحقق الروتيني من نظرية المجموعات.

4. النتائج

حجم الأثر (Artifact Size): تتكون المكتبة من 8,324 سطراً من كود Lean و 706 نظرية مثبتة.
تفصيل المكونات:
- الحساب العلاقي: ~~2,534 سطر كود (~~172 نظرية).
- الأعداد الطبيعية: ~~1,260 سطر كود (~~199 نظرية).
- التضمينات/التماثلات: ~~1,626 سطر كود (~~31 نظرية).
سهولة الاستخدام: توضح دراسة الحالة أن الإطار ينجح في تقليل الاحتكاك في الصياغة على مستوى المجموعات. يمكن للمستخدمين كتابة براهث تشبه الحجج الرياضية القياسية دون الحاجة لإثبات أن كل تركيب للعلاقات هو علاقة صالحة يدوياً.
التوافقية: القدرة على التبديل بين ZFSet والنوع الأصلي Type تسمح بإعادة استخدام تاكتيكات الجبر في Mathlib (مثل ring) على كائنات نظرية المجموعات.

5. الأهمية

الربط بين الأسس: يقوم ZFLean بفعالية بالتوفيق بين الرؤى "النظرية للمجموعات" و"النوعية" للرياضيات ضمن مساعد إثبات واحد. فهو يسمح للرياضيين باختيار الأساس الأكثر طبيعية لمشكلة معينة (المجموعات الامتدادية مقابل الأنواع البنائية) دون فقدان الوصول إلى نظام الأتمتة الخاص بهم.
سهولة الاستخدام (Ergonomics): من خلال أتمتة الشروط الجانبية المملة المتأصلة في نظرية المجموعات (إثباتات العضوية، وصحة العلاقة الوظيفية)، فإنه يجعل تطوير ZFC في Lean ممكناً لغير الخبراء وعملياً للصياغات واسعة النط scale.
القابلية للتوسع: يسمح التصميم المجزأ (الحساب العلاقي + الكائنات المعيارية + الجسور) بالتوسع السهل. العمل المستقبلي يتضمن صياغة الأعداد الحقيقية (عبر متتاليات كوشي أو قطع ديدكايند) والتحليل الأساسي.
المقارنة: على عكس Isabelle/ZF (حيث نظرية المجموعات هي منطق كائن منفصل) أو تطورات نظرية المجموعات في Rocq (التي غالباً ما تفتقر إلى التكامل العميق مع أتمتة نظرية الأنواع)، يقدم ZFLean نهجاً هجيناً يحافظ على البراهث عند مستوى المجموعات مع الاستفيد من البنية التحتية النوعية الأصلية لـ Lean.

في الختام، يوفر ZFLean إطار عمل قوياً، مريحاً، ومتوافقاً للقيام بالرياضيات الأساسية في ZFC داخل Lean 4، مما يقلل بنجاح من حاجز الدخول إلى الصياغة النظرية للمجموعات مع الحفاظ على التوافق مع منظومة Mathlib الأوسع.