يستخدم مجتمع صغير من علماء الرياضيات اللين لبناء قاعدة رقمية جديدة. يأملون في تأمين مستقبل مجالهم العلمي.
كل يوم ، يلتقي العشرات من علماء الرياضيات المتشابهين في التفكير في دردشة Zulip للعمل على ما يعتقدون أنه يشكل مستقبل مجالهم العلمي.
كلهم من عشاق برنامج Lean . إنها أداة إثبات نظرية تفاعلية قادرة ، من حيث المبدأ ، على مساعدة علماء الرياضيات في كتابة البراهين. ومع ذلك ، لهذا ، يجب على علماء الرياضيات إدخال القواعد الرياضية يدويًا في قاعدة البرنامج ، مما يجعل المعرفة التي تم جمعها على مدى آلاف السنين في شكل يمكن للكمبيوتر فهمه.
بالنسبة للعديد من المشاركين في المشروع ، تتطلب فوائده القليل من الشرح أو لا تتطلب أي تفسير.
قال كيفين بازارد: "على المستوى الأساسي ، من الواضح أنه بمجرد أن يتم رقمنة شيء ما ، يمكن استخدامه بطرق جديدة"من إمبريال كوليدج لندن. "وسنقوم برقمنة الرياضيات ، وجعلها أفضل."
رقمنة الرياضيات حلم قديم. وتتراوح الفوائد المتوقعة من هذا من التافه - فحص واجبات الطلاب المنزلية بأجهزة الكمبيوتر - إلى الاستثنائي: استخدام الذكاء الاصطناعي لاكتشافات رياضية جديدة وإيجاد حلول جديدة للمشكلات القديمة. يعتقد علماء الرياضيات أن مبرهنات النظرية التلقائية ستكون قادرة أيضًا على مراجعة المقالات المقدمة إلى المجلات ، والعثور على الأخطاء التي يفوتها المراجعون البشريون في بعض الأحيان ، والانخراط في العمل الفني الممل المتمثل في ملء الدليل بجميع التفاصيل اللازمة.
لكن أولاً ، يحتاج علماء الرياضيات الذين يجتمعون في محادثة إلى تزويد اللين بالمعرفة في إطار الرياضيات المدرسية ، وحتى الآن لم تكتمل هذه المهمة إلا نصفها. في المستقبل القريب ، من غير المرجح أن يتمكن Lean من حل المشكلات المفتوحة ، لكن الأشخاص الذين يعملون في القاعدة هم على يقين تقريبًا من أنه في غضون سنوات قليلة فقط سيتعلم البرنامج على الأقل فهم مشكلات مستوى الامتحان في المدرسة الثانوية.
من تعرف؟ لا يمتلك علماء الرياضيات المشاركون في المشروع دائمًا فكرة واضحة عما يمكن أن تكون الرياضيات الرقمية مفيدة فيه.
قال سيباستيان جوسيل من جامعة رين "لا نعرف بالضبط إلى أين نحن ذاهبون" .
أنت تخطط ، أعمال العجاف
خلال الصيف ، عقدت مجموعة من مستخدمي Lean ذوي الخبرة ندوة عبر الإنترنت بعنوان " Lean for Curious Mathemists ". في الدرس الأول ، أوضح سكوت موريسون من جامعة سيدني كيف يمكنك كتابة إثبات باستخدام أحد البرامج.
بدأ بكتابة البيان الذي أراد إثباته بعبارات Lean. في لغة البشر ، كان يعني "هناك عدد لا حصر له من الأعداد الأولية". هناك عدة طرق لإثبات هذا الادعاء ، لكن موريسون أراد استخدام نسخة معدلة قليلاً من الدليل الأول الذي وجده إقليدس من 300 قبل الميلاد. في الإثبات ، يتم ضرب جميع الأعداد الأولية المعروفة ، وبعد إضافة 1 ، يتم الحصول على رقم أولي جديد (إما المنتج نفسه أو أحد مقسوماته سيكون أوليًا). اعتمد اختيار موريسون على إحدى القواعد الأساسية لاستخدام اللين: يجب أن يأتي المستخدم بالفكرة الرئيسية للإثبات بنفسه.
قال موريسون في مقابلة "أنت مسؤول عن التخمين الأول".
بعد إدخال التأكيد واختيار الإستراتيجية ، حدد موريسون هيكل الإثبات في بضع دقائق. حدد سلسلة من الخطوات الوسيطة ، كان من السهل نسبيًا إثبات كل منها. بينما لا تستطيع اللين تقديم استراتيجية إثبات عامة ، إلا أنها يمكن أن تساعدك على تنفيذ خطوات صغيرة وملموسة. بتقسيم الدليل إلى مهام فرعية يمكن الوصول إليها ، كان موريسون يشبه إلى حد ما طاهٍ يوجه الطهاة العاديين إلى تقطيع البصل أو غلي الماء. قال موريسون: "هذا هو المكان الذي تأمل فيه أن يتولى Lean زمام الأمور ويبدأ في مساعدتك".
ينجز Lean المهام الوسيطة باستخدام عمليات آلية تسمى التكتيكات. هذه نوع من الخوارزميات القصيرة المصممة لأداء مهام محددة للغاية.
من خلال العمل مع الدليل ، أطلق موريسون تكتيكًا يسمى البحث في المكتبة. قامت بتمشيط قاعدة بيانات الرياضيات الخاصة بالبرنامج وأعادت العديد من النظريات التي اعتقدت أنها يمكن أن تملأ الفجوات في قسم معين من البرهان. تكتيكات مختلفة تؤدي مهام رياضية مختلفة. أحدهما ، Linarith ، يمكن أن يأخذ مجموعة من المتباينات لعددين حقيقيين ، على سبيل المثال ، ويؤكد حقيقة المتباينة الجديدة ، والتي تتضمن الرقم الثالث: إذا كانت a 2 و b أكبر من a ، فإن 3a + 4b أكبر من 12. الآخر يفعل معظم العمل مع القواعد الجبرية الأساسية مثل الترابطية.
قالت أميليا ليفينجستون ، طالبة الرياضيات في إمبريال كوليدج لندن والتي تدرس Lean مع Buzzard: "قبل عامين في Lean ، كان لابد من تطبيق الترابط يدويًا". - ثم كتب أحدهم تكتيكًا يفعل ذلك من أجلك. أنا سعيد في كل مرة أستخدمها ".
إجمالاً ، استغرق الأمر من موريسون 20 دقيقة لإكمال إثبات إقليدس. هنا وهناك أكمل التفاصيل بنفسه. في بعض الأحيان قام التكتيك بذلك من أجله. بعد كل خطوة ، تحقق Lean من اتساق الإثبات وفقًا للقواعد المنطقية المضمنة المكتوبة بلغة رسمية تسمى نظرية النوع التابع .
"يبدو أنه تطبيق سودوكو. قال Buzzard ، "إذا قمت بخطوة خاطئة ، فإنها تصدر صوت تنبيه". نتيجة لذلك ، أكد لين قابلية عمل دليل موريسون.
لقد كان تمرينًا ممتعًا للغاية - كما هو الحال عادةً عندما تفعل التكنولوجيا شيئًا من أجلك. ومع ذلك ، فإن دليل إقليدس موجود منذ أكثر من 2000 عام. الأسئلة التي يطرحها علماء الرياضيات اليوم معقدة للغاية لدرجة أن اللين لا يستطيع حتى فهم الأسئلة ، ناهيك عن المساعدة في الإجابة عليها.
قالت هيذر ماكبث من جامعة فوردهام ، أحد مستخدمي Lean: "من المحتمل أن تستغرق هذه الأداة عقودًا للمساعدة في البحث" .
لذا ، قبل أن يتمكن علماء الرياضيات من العمل مع Lean في الأسئلة التي تهمهم حقًا ، عليهم إضافة المزيد من قواعد الرياضيات إلى البرنامج. وهذه ، في الواقع ، مهمة بسيطة إلى حد ما.
تشريح برنامج الإثبات: يساعد Lean علماء الرياضيات على إثبات النظريات من خلال التحقق من العمل وأتمتة بعض الخطوات في البراهين.
1) يصف عالم الرياضيات البنية الأساسية للإثبات ، ويكتب تسلسل الخطوات في Lean.
2) مكتبة الرياضيات لبرامج الرياضيات لديها مجموعة من التكتيكات التي تؤدي خطوات هذا الإثبات. يواصل علماء الرياضيات إضافة بيانات جديدة إلى الرياضيات. تمت إضافة نظريات مثبتة إلى mathlib.
3) تتحقق خوارزمية Kernel من صحة الإثبات باستخدام قواعد بسيطة.
* أصبح الأخطبوط بطريقة ما تسمية للمشاعر المبهجة في مجتمع اللين.
قال موريسون: "لكي يتمكن Lean من فهم شيء ما ، يحتاج الناس إلى ترجمة كتب الرياضيات المدرسية إلى صيغة يستطيع البرنامج فهمها".
لسوء الحظ ، لا تعني بساطة المشكلة أنه من السهل إكمالها - نظرًا لأن الكثير من الرياضيات غير مغطاة في الكتب المدرسية.
المعرفة المتناثرة
إذا لم تكن قد درست الرياضيات المتقدمة ، فقد تبدو هذه المنطقة دقيقة وموصوفة جيدًا لك. الجبر ، حساب التفاضل ، التحليل الرياضي - كل شيء يتبع من كل شيء ، وهناك إجابات على جميع الأسئلة ، مدرجة في نهاية الكتاب المدرسي.
ومع ذلك ، فإن الرياضيات في المناهج المدرسية ومناهج الكلية وحتى جزء كبير من الجامعة هي جزء صغير من كل المعرفة. معظمهم ليسوا منظمين بشكل جيد.
هناك مجالات ضخمة ومهمة في الرياضيات لم يتم وصفها بشكل كامل. يتم تخزينها في أذهان عدد قليل من الأشخاص الذين تعلموا مجالهم الفرعي من الرياضيات من الأشخاص الذين تعلموا ذلك من أولئك الذين اخترعوه - أي أنهم موجودون على أساس الفولكلور.
هناك مجالات أخرى تم فيها تدوين المادة الأساسية ، لكنها معقدة للغاية وطويلة بحيث لم يتمكن أحد من التحقق من صحتها. بدلاً من ذلك ، يؤمن علماء الرياضيات به ببساطة.
“نحن نعتمد على سمعة المؤلف. قال باتريك ماسوت من جامعة باريس ساكلاي: " نحن نعلم أنه عبقري وشخص دقيق ، لذا فإن الدليل صحيح على الأرجح" .
هذا هو أحد الأسباب التي تجعل برامج إثبات النظريات جذابة للغاية. تجبر ترجمة الرياضيات إلى لغة مفهومة بواسطة الكمبيوتر علماء الرياضيات على تصنيف معارفهم في النهاية وتحديد جميع الأشياء بدقة.
آسيا مابوبيمن المعهد الحكومي الفرنسي للبحوث في المعلوماتية والأتمتة تذكر المرة الأولى التي أدركت فيها إمكانات مثل هذه المكتبة الرقمية المنظمة: "لقد أسرتني إمكانية التغطية النظرية لجميع الأدبيات الرياضية باستخدام لغة المنطق البحت ، وتخزين المكتبة الرياضية بأكملها في جهاز كمبيوتر ، والتحقق والبحث عن البيانات الموجودة فيها بمساعدة البرامج ".
اللين ليس البرنامج الأول الذي يمتلك هذه الإمكانات. أولها ، Automath ، ظهر في الستينيات ، و Coq ، أحد أكثرها شهرة اليوم ، ظهر في عام 1989. مستخدمو Coq قاموا بإضفاء الطابع الرسمي على الكثير من الرياضيات في لغة البرنامج ، لكن هذا العمل كان لامركزيًا وغير منظم جيدًا. عمل علماء الرياضيات فقط في المشاريع التي تهمهم ، وحددوا فقط تلك الأشياء التي يحتاجونها لعملهم الخاص ، وغالبًا ما يصفونها بطرق فريدة. نتيجة لذلك ، تبدو مكتبات Coq مزدحمة ، مثل مخطط لمدينة نمت بشكل طبيعي.
قال مابوبي ، الذي كان ناشطًا في البرنامج: "كوك رجل عجوز يعاني من ندوب اليوم". "لقد دعمه الكثير من الناس لفترة طويلة ، وبفضل تاريخه الطويل ، أصبحت عيوبه معروفة الآن".
في عام 2013 ، أطلق ليوناردو دي مورا ، الباحث في Microsoft ، مشروع Lean. يعكس اسمها [lean] رغبة دي مور في إنشاء برنامج فعال ونظيف. وافترض أن البرنامج سيكون أداة للتحقق من دقة كود البرامج الأخرى وليس الرياضيات. ومع ذلك ، فقد تبين أن التحقق من صحة البرنامج يشبه إلى حد كبير التحقق من الإثبات.
قال دي مور: "أنشأنا اللين لأننا مهتمون بتطوير البرمجيات ، وهناك تشابه بين إنشاء الرياضيات وكتابة الكود".
هيذر ماكبث من جامعة فوردهام ، أحد مستخدمي Lean
في وقت إصدار Lean ، كان هناك عدد غير قليل من البرامج المساعدة الأخرى ، بما في ذلك Coq ، الذي يشبه إلى حد كبير برنامج Lean. يعتمد الأساس المنطقي لكلا البرنامجين على نظرية الأنواع التابعة. ومع ذلك ، يوفر Lean فرصة للبدء من جديد.
جذبت علماء الرياضيات بسرعة. لقد استخدموها بحماس لدرجة أنهم بدأوا في قضاء كل وقت فراغ De Moore في طرح أسئلتهم حول التطور في مجال الرياضيات. "لقد سئم قليلا من علماء الرياضيات البارزين وقال - لماذا لا تقومون يا رفاق بإنشاء مستودع منفصل؟" قال موريسون.
أنشأ علماء الرياضيات هذه المكتبة في عام 2017. أطلقوا عليها اسم "الماثلب" وشرعوا بحماسة في ملئها بالمعرفة الرياضية العالمية ، وخلق ما يشبه نظير مكتبة الإسكندرية.في القرن الحادي والعشرين. قام علماء الرياضيات بإنشاء وتنزيل مقتطفات من الرياضيات الرقمية ، وإنشاء كتالوج تدريجي لـ Lean. ونظرًا لأن mathlib كان جديدًا ، فيمكنهم التعلم من قيود الأنظمة السابقة مثل Coq ، وتتبع كيفية تنظيم المواد.
قال ماكبث: "هناك محاولة متعمدة لإنشاء مكتبة رياضية متجانسة ، وجميع أجزاءها ستعمل مع بعضها البعض".
المثلب السكندري
تحتوي الصفحة الرئيسية لمشروع mathlib على رسوم بيانية توضح تقدم المشروع في الوقت الفعلي. يحتوي المشروع على قائمة بالقادة الذين يستثمرون فيه أكثر ، مرتبة حسب عدد سطور الكود [في المقام الأول ، بالمناسبة ، عالم الرياضيات الروسي يوري كودرياشوف / تقريبًا. ترجمة.]. يتم أيضًا حساب إجمالي عدد العناصر الرياضية الرقمية: في بداية أكتوبر ، تحتوي على 18756 تعريفًا و 39157 نظرية.
يمكن خلط كل مكونات الرياضيات هذه لإنشاء رياضيات داخل اللين. حتى الآن ، مداها محدود للغاية ، على الرغم من الأرقام التي تبدو مثيرة للإعجاب. لا يوجد شيء تقريبًا في مجالات التحليل المعقد أو المعادلات التفاضلية - وهذان عنصران أساسيان في العديد من مجالات الرياضيات العليا. بالإضافة إلى ذلك ، لا يعرف البرنامج بعد ما يكفي حتى لوصف أيًا من مشاكل الألفية - المشكلات الرياضية التي حددها معهد كلاي الرياضي في عام 2000 على أنها "مشاكل كلاسيكية مهمة لم يتم حلها لسنوات عديدة".
`` Mathlib '' تملأ ببطء ولكن بثبات. يسير العمل بروح العمل الجماعي. في دردشة Zulip ، يختار علماء الرياضيات التعاريف لإضفاء الطابع الرسمي عليها ، ويواجهون تحديًا لكتابتها ، وتقديم ملاحظات فورية حول عمل الآخرين.
قال ماكبث: "يمكن لأي عالم رياضيات بحثي أن يدرس الرياضيات ويضع قائمة بأربعين شيئًا غير موجود". - لذلك قرر سد أي من هذه النواقص. والمتعة الفورية مضمونة - سيقرأ شخص ما عملك ويترك تعليقًا عنه في غضون 24 ساعة ".
تأتي العديد من الإضافات صغيرة - كما اكتشفت صوفي موريلمن مدرسة ليون العادية خلال الندوة عبر الإنترنت "العجاف لعلماء الرياضيات الفضوليين". أعطى منظمو المؤتمر للمشاركين بيانات رياضية بسيطة نسبيًا يجب إثباتها في Lean كممارسة. من خلال العمل مع أحدهم ، أدركت موريل أن إثباتها يتطلب ليمما - نتيجة وسيطة صغيرة - لم يتم العثور عليها في حساب mathlib.
"لقد كانت قطعة صغيرة من الجبر الخطي ، والتي ، لسبب ما ، لم تكن موجودة بعد. قالت موريل ، التي أدخلت اللمة المطلوبة في ثلاثة أسطر في القاعدة ، "يحاول الأشخاص الذين يملأون معلومات الحساب استيعاب كل شيء ، لكن لا يمكنك توقع كل الخيارات".
المساهمات الأخرى أكثر أهمية. خلال العام الماضي ، كان جوسيل يعمل على تحديد مشعب سلس لـ mathlib. المشعبات الملساء هي مجموعات (مثل الخطوط أو الدوائر أو أسطح الكرة) التي تلعب دورًا أساسيًا في دراسة الهندسة والطوبولوجيا. غالبًا ما يلعبون دورًا مهمًا في المشكلات من مجالات مثل نظرية الأعداد وحساب التفاضل والتكامل. معظم البحوث الرياضية مستحيلة بدونها.
ومع ذلك ، يمكن أن تختبئ المشعبات السلسة تحت أشكال مختلفة - كل هذا يتوقف على السياق. يمكن أن يكون لها عدد محدود أو لا حصر له من الأبعاد ، أو أن يكون لها حدود أو لا تحتوي عليها ، ويمكن تحديدها عبر أنظمة أعداد مختلفة - على مجموعة حقيقية أو معقدة أو p-adicأعداد. إن تعريف التنوع السلس يشبه تعريف الحب: فأنت تتعرف عليه عندما تقابله ، لكن أي تعريف صارم سوف يسقط بالتأكيد بعض الأمثلة الأكثر وضوحًا لهذه الظاهرة.
قال جوسيل: "عند تحديد الأشياء الأساسية ، لا يتعين عليك اتخاذ أي خيارات". "ولكن يمكن إضفاء الطابع الرسمي على الأشياء الأكثر تعقيدًا من 10 إلى 20 طريقة مختلفة."
يحتاج Gösel إلى الحفاظ على توازن الخصوصية والتعميم. قال "كانت لدي قاعدة - أردت أن أكون قادرًا على تحديد 15 استخدامًا مختلفًا للمشعبات". "في الوقت نفسه ، لم أكن أرغب في أن يكون التعريف عامًا جدًا ، وإلا فسيكون من المستحيل التعامل معه".
يتناسب التعريف الذي طوره مع 1600 سطر من التعليمات البرمجية - وهو عدد كبير جدًا من التعريف من Mathlib ، ولكن ربما ليس كثيرًا مقارنة بجميع الاحتمالات الرياضية التي يفتحها لـ Lean.
قال: "الآن بعد أن حصلنا على اللغة التي نحتاجها ، يمكننا البدء في إثبات النظريات".
إن العثور على التعريف الصحيح لشيء بدرجة عمومية صحيحة هو المهنة الرئيسية لعلماء الرياضيات الذين يملئون حساب "ماتليب". يأمل منشئو المكتبة في تحديد الأشياء بطريقة مفيدة اليوم ، وفي نفس الوقت مرنة بدرجة كافية بحيث يمكن استخدام هذه الكائنات بطريقة لا يمكن التنبؤ بها اليوم.
قال ماكبث: "تم التأكيد على الحاجة إلى أن يكون كل شيء مفيدًا للاستخدام في المستقبل البعيد".
ولدت Perfectoids من الممارسة
لكن اللين ليس مجرد أداة مفيدة - فهو يمنح علماء الرياضيات فرصة لإعادة الانخراط في عملهم. لا تزال ماكبث تتذكر المرة الأولى التي جربت فيها برنامجًا للمساعدة في كتابة البراهين. كان عام 2019 وكان البرنامج Coq (على الرغم من أنه الآن Lean). لم تستطع التوقف.
قالت "في عطلة نهاية أسبوع مجنونة ، عملت مع هذا البرنامج لمدة 12 ساعة متواصلة". "لقد كان إدمان حقيقي".
يصف علماء رياضيات آخرون تجاربهم بطريقة مماثلة. يقولون إن Lean يشبه لعبة كمبيوتر - وصولاً إلى نفس هرمونات المكافأة التي تجعل من الصعب وضع جهاز التحكم في اللعبة جانبًا. قال ليفينغستون: "يمكنك القيام بذلك لمدة 14 ساعة في اليوم دون الشعور بالتعب وفي حالة مرتفعة طوال اليوم". "تحصل على ردود فعل إيجابية في كل وقت."
سيباستيان جوسيل
يدرك مجتمع اللين أنه بالنسبة للعديد من علماء الرياضيات ، لا توجد ببساطة مستويات كافية في برنامجهم.
قال كريستيان سيجيدي ، أحد مبرمجي Google الذي يعمل على أنظمة الذكاء الاصطناعي ، والذي يحلم بأن يكون قادرًا على قراءة الكتب المدرسية الرياضيات وإضفاء الطابع الرسمي عليها: "إذا حددت النسبة المئوية للرياضيات الرسمية ، فسأقول إن أقل من واحد من ألف بالمائة جاهز حتى الآن".
لكن علماء الرياضيات يزيدون هذه النسبة. إذا كان برنامج `` Mathlib '' يحتوي اليوم على معظم المواد التي يدرسها طلاب السنة الثانية بالجامعة ، فإن المشاركين في المشروع يأملون في إضافة بقية البرنامج في غضون سنوات قليلة - وسيكون هذا إنجازًا كبيرًا.
قال بازارد: "في كل 50 عامًا من هذه الأنظمة ، لم يقترح أحد على الإطلاق: فلنجلس وننظم قاعدة معرفية متسقة للرياضيات تصف مادة المعهد". "نحن نبتكر شيئًا يمكنه فهم أسئلة امتحان المعهد - لم يحدث هذا من قبل."
من المحتمل أن تمر عقود قبل أن يتطابق محتوى mathlib مع مكتبة البحث ، لكن مستخدمي Lean يبرهنون على الأقل على الإمكانية النظرية لإنشاء مثل هذا الكتالوج - وتحقيق هذا الهدف يعتمد ببساطة على إدخال جميع الرياضيات في قاعدة البيانات في شكل رمز البرنامج.
تحقيقًا لهذه الغاية ، نفذ بازارد وماسو ويوهان كوملين من جامعة فرايبورغ في ألمانيا العام الماضي مشروعًا يثبت جدوى هذا الحلم. وقد أجلوا مؤقتًا الملء التدريجي للقاعدة بمادة المعهد وانتقلوا إلى مناطق متقدمة. كان هدفهم هو تحديد أحد أعظم الابتكارات في الرياضيات في القرن الحادي والعشرين - كائن مثل "الفضاء المثالي" الذي طوره بيتر شولز من جامعة بون على مدى السنوات العشر الماضية . في عام 2018 ، حصل على جائزة فيلدز عن عمله ، وهي أكبر جائزة في الرياضيات.
أراد Buzzard و Masso و Commelin إثبات أنه ، على الأقل من حيث المبدأ ، يمكن أن يعمل Lean مع الرياضيات التي يهتم بها علماء الرياضيات حقًا. قال مابوبي: "لقد أخذوا شيئًا معقدًا وجديدًا للغاية وأظهروا أن هذه الأشياء يمكن التلاعب بها ببرنامج للمساعدة في كتابة البراهين".
كيفن بازارد Kevin Buzzard
لتعريف الفضاء المثالي ، احتاج ثلاثة علماء رياضيات إلى الجمع بين أكثر من 3000 تعريف للكائنات الرياضية و 30000 اتصال بينهم. امتدت التعريفات عبر العديد من مجالات الرياضيات ، من الجبر إلى الطوبولوجيا والهندسة. كان وضعهم معًا في تعريف واحد دليلًا قويًا على النمو في تعقيد الرياضيات بمرور الوقت - ولماذا من المهم جدًا تصحيح أسس الرياضيات.
قال ماكبث: "تتطلب العديد من مجالات الرياضيات المتقدمة منك معرفة جميع أنواع الرياضيات التي يتم تدريسها للطلاب".
نجح الثالوث في تحديد الفضاء المثالي ، ولكن حتى الآن لا يوجد سوى القليل من علماء الرياضيات الذين يمكنهم فعل ذلك. مطلوب العديد من التعريفات الرياضية في اللين ، حتى يتمكن البرنامج على الأقل من صياغة تلك الأسئلة الصعبة التي تنشأ فيها هذه المساحات المثالية.
قال ماسو: "من السخف أن يعرف Lean ما هو الفضاء المثالي ، لكنه لا يعرف التحليل المعقد".
يتفق Buzzard معه ، واصفًا إضفاء الطابع الرسمي على الفضاء المثالي بأنه "وسيلة للتحايل" - وهي خدعة تُظهر أحيانًا التقنيات الجديدة لإثبات فائدتها. وهذه المرة نجحت الحيلة.
قال ماسو: "ليس عليك التفكير في أنه بفضل عملنا ، بدأ جميع علماء الرياضيات على الأرض في استخدام البرامج للمساعدة في كتابة البراهين ، لكنني أعتقد أن العديد منهم لاحظوا هذا الاحتمال وبدأوا في طرح الأسئلة".
سوف يمر وقت طويل قبل أن يصبح اللين جزءًا حقيقيًا من البحث الرياضي. ومع ذلك ، هذا لا يعني أن البرنامج اليوم هو صورة من الخيال العلمي. يقارن علماء الرياضيات المشاركون في تطويره عملهم بوضع خطوط السكك الحديدية الأولى - البداية الضرورية لمشروع مهم ، حتى لو كانوا هم أنفسهم غير قادرين على ركوب المسار.
قال ماكبث: "سيكون شيئًا رائعًا أنه يستحق العناء اليوم". "أنا أستثمر وقتي فيها اليوم حتى يتمكن شخص ما في المستقبل من الاستمتاع بتجربة رائعة في العمل معها".