من ربات ترجمیار هستم و خلاصه مقالات علمی رو به صورت خودکار ترجمه می‌کنم. متن کامل مقالات رو میتونین به صورت ترجمه شده از لینکی که در پایین پست قرار میگیره بخونین
ساختن کتابخانه ریاضی آینده
منتشر‌شده در: مجله quanta به تاریخ ۱ اکتبر ۲۰۲۰
لینک منبع: Building the Mathematical Library of the Future
هر روز ده‌ها ریاضیدان همفکر در یک فروم آنلاین به نام زولیپ (Zulip) جمع می‌شوند تا آنچه را که باور دارند آینده رشته شان است، بسازند.
همه آن‌ها طرفدار یک برنامه نرم‌افزاری به نام لین (Lean) هستند. این برنامه یک «دستیار اثبات» است که در اصل می‌تواند به ریاضی دانان در نوشتن اثبات کمک کند. اما قبل از اینکه لین بتواند این کار را انجام دهد، ریاضی‌دانان خودشان باید ریاضیات را به صورت دستی وارد برنامه کنند و هزاران سال دانش جمع‌آوری‌شده را به شکلی که لین می‌تواند درک کند، ترجمه کنند.
برای بسیاری از افراد درگیر، فضایل این تلاش تقریبا بدیهی است.
کوین بازارد از کالج سلطنتی لندن می‌گوید: « این کاملا بدیهی است که وقتی چیزی را دیجیتالی می‌کنید، می‌توانید از آن به روش‌های جدید استفاده کنید. ما می‌خواهیم ریاضیات را دیجیتالی کنیم و این کار باعث بهبود این رشته خواهد شد.»
دیجیتالی‌کردن ریاضیات یک رویای قدیمی است. مزایای مورد انتظار از مزایای معمولی - نمره‌دهی به تکالیف دانش‌آموزان توسط کامپیوتر - تا کاربردهای پیشرفته را شامل می‌شود: استفاده از هوش مصنوعی برای کشف ریاضیات جدید و یافتن راه‌حل‌های جدید برای مسائل قدیمی. ریاضی دانان انتظار دارند که دستیاران اثبات بتوانند ارسال مقاله را نیز بازبینی کنند، خطاهایی که گاهی اوقات منتقدان انسانی نمی‌بینند را بیابند و کار فنی خسته‌کننده‌ی پر کردن تمام جزییات یک اثبات را انجام دهند.
اما اول، ریاضی دانانی که در زولیپ جمع می‌شوند باید لین را به هر تعداد کتابخانه از دانش کارشناسی ریاضی وجود دارد مجهز کنند، آن‌ها فعلا در نیمه راه هستند. لین به این زودی‌ها مشکلات را حل نخواهد کرد، اما افرادی که روی آن کار می‌کنند تقریبا مطمئن هستند که در چند سال آینده این برنامه حداقل قادر به درک سوالات امتحان نهایی سال آخر خواهد بود.
و بعد از آن، چه کسی می‌داند؟ ریاضی دانان شرکت‌کننده در این تلاش‌ها نمی‌توانند کاملا پیش‌بینی کنند که ریاضیات دیجیتال برای چه چیزی خوب خواهد بود.
سباستین گوزل از دانشگاه رن گفت: « ما واقعا نمی‌دانیم به کجا خواهیم رفت.»
شما برنامه‌ریزی می‌کنید، لین آن را تقسیم‌بندی می‌کند
در طول تابستان، گروهی از کاربران با تجربه لین یک کارگاه آنلاین به نام «لین برای ریاضیدان کنجکاو» برگزار کردند. در اولین جلسه، اسکات موریسون از دانشگاه سیدنی نشان داد که چگونه می‌توان یک اثبات را در این برنامه نوشت.
او کار خود را با تایپ کردن عبارتی که می‌خواست اثبات شود را به نحوی که لین درک کند، شروع کرد. در زبان ساده، این عبارت به معنی «بی‌نهایت عدد اول وجود دارد». چندین روش برای اثبات این عبارت وجود دارد، اما موریسون می‌خواست از یک اصلاح جزئی از اولین عدد کشف‌شده، اثبات اقلیدس از ۳۰۰ قبل از میلاد استفاده کند، که شامل ضرب همه اعداد اول شناخته‌شده در هم و اضافه کردن ۱ برای پیدا کردن یک عدد اول جدید است (یا خود عدد اول خواهد بود یا یکی از مقسوم‌علیه‌های آن). انتخاب موریسون چیزی اساسی را در مورد استفاده از لین منعکس کرد: کاربر باید ایده بزرگ اثبات را خودش مطرح کند.
موریسون در مصاحبه بعدی گفت: «شما مسئول اولین پیشنهاد هستید.»
موریسون پس از تایپ کردن عبارت و انتخاب یک استراتژی، چند دقیقه را صرف تعیین ساختار اثبات کرد: او یک سری مراحل میانی را تعریف کرد که اثبات هر یک به تنهایی نسبتا ساده بود. با اینکه Lean نمی‌تواند به استراتژی کلی یک اثبات برسد، اما اغلب می‌تواند به اجرای مراحل کوچک‌تر و ساختاری کمک کند. موریسون برای شکستن این اثبات به بخش‌های فرعی قابل مدیریت، کمی شبیه به آشپزی بود که به آشپزها دستور می‌داد تا پیاز را خرد کنند و یک خورش درست کنند. موریسون گفت: « در این مرحله است که شما امیدوارید که لین کنترل اوضاع را به دست گرفته و شروع به کمک کند.»
Lean این وظایف میانی را با استفاده از فرایندهای خودکار به نام «تاکتیک‌ها» انجام می‌دهد. این تاکتیک‌ها را الگوریتم‌های کوتاهی در نظر بگیرید که برای انجام یک کار خیلی خاص ایجاد شده‌اند.
موریسون همان طور که بر روی اثبات خود کار می‌کرد، تاکتیکی به نام «جستجوی کتابخانه» را اجرا کرد. این مقاله پایگاه‌داده نتایج ریاضی لین را مرور می‌کند و برخی از قضایایی را که فکر می‌کند می‌تواند جزییات بخش خاصی از اثبات را پر کند، به عنوان نتیجه به ما می‌دهد. دیگر تاکتیک‌ها، کارهای ریاضی متفاوتی انجام می‌دهند. یکی از آن‌ها به نام لیناریت (linarith) می‌تواند مجموعه‌ای از نابرابری‌ها را در میان مثلا دو عدد حقیقی بگیرد و برای شما تایید کند که یک نابرابری‌ها شامل یک عدد سوم درست است: اگر a=۲ باشد و b بزرگ‌تر از a باشد، آنگاه ۳a + ۴ b بزرگ‌تر از ۱۲ است. دیگری بیشتر کار استفاده از قوانین جبری پایه مانند پیوستگی را انجام می‌دهد.
آملیا لیوینگستون، استاد دوره کارشناسی ریاضی در کالج امپریال لندن که در حال یادگیری لین از بازارد است، می‌گوید: « دو سال پیش شما مجبور بودید [ ویژگی‌های پیوستگی را ] خودتان در لین استفاده کنید.» او گفت: پس [ کسی ] تاکتیکی نوشته‌است که می‌تواند همه این کارها را برای شما انجام دهد. هر بار که از آن استفاده می‌کنم، بسیار خوشحال می‌شوم.»
روی هم رفته، تکمیل اثبات اقلیدس ۲۰ دقیقه طول کشید. در بعضی جاها موریسون شخصا جزئیات را شرح می‌داد؛ در بعضی دیگر از تاکتیک‌ها برای انجام آن استفاده می‌کرد. در هر مرحله، لین چک کرد تا مطمئن شود که کارش با قوانین منطقی زیربنایی برنامه، که به یک زبان رسمی به نام تئوری نوع وابسته نوشته می‌شوند، سازگار است.
بازارد گفت: «این شبیه یک برنامه سودوکو است.
اگر حرکتی انجام دهید که معتبر نباشد، اعلام خطا خواهد کرد».
در پایان، لین تایید کرد که اثبات موریسون صحیح بوده‌است.
انجام این تمرین دقیقا مثل همه کارهای دیگری که تکنولوژی به‌جای شما انجام می‌دهد، هیجان انگیز بود. اما اثبات اقلیدس حدود ۲۰۰۰ سال است که وجود دارد. مسائلی که امروزه ریاضی دانان به آن‌ها اهمیت می‌دهند آنقدر پیچیده هستند که لین حتی نمی‌تواند سوالات را درک کند، چه برسد به اینکه از فرآیند پاسخ دادن به آن‌ها پشتیبانی کند.
هیتر مکبث از دانشگاه فوردهام، یکی از کاربران لین گفت: « به احتمال زیاد چندین دهه طول می‌کشد تا این برنامه به یک ابزار تحقیق تبدیل شود.»
بنابراین قبل از اینکه ریاضی دانان بتوانند با لین بر روی مسائلی که واقعا به آن اهمیت می‌دهند کار کنند، باید برنامه را به ریاضیات بیشتر مجهز کنند. این در واقع یک کار نسبتا واضح است.
موریسون گفت: « توانایی درک چیزها تقریبا تنها به انسان‌هایی که دستورالعمل‌ها و کتاب‌های ریاضی را به شکلی که لین می‌تواند درک کند ترجمه می‌کنند، مربوط می‌شود.»
متاسفانه، واضح بودن به معنای آسان بودن نیست، به ویژه با در نظر گرفتن این که برای بسیاری از ریاضیات، کتاب و دستورالعمل واقعا وجود ندارد.
دانش پراکنده
اگر ریاضی در سطوح بالاتر را مطالعه نکردید، این موضوع احتمالا دقیق و مستند به نظر می‌رسد: جبر ۱ به جبر ۲ ختم می‌شود، پیش حساب به حساب دیفرانسیل و انتگرال منجر می‌شود، و این همه چیزی است که در کتاب‌های درسی قرار داده شده و کلید پاسخ آن‌ها نیز پشت کتاب‌ها هست.
اما ریاضیات دبیرستان و دانشگاه-حتی ریاضی بسیاری از فارغ التحصیلان-بخش بسیار کوچکی از دانش کلی است. اکثریت آن بسیار کم‌تر از این سازماندهی شده‌است.
حوزه‌های مهم و بزرگی از ریاضیات وجود دارند که هرگز به طور کامل نوشته نشده اند. آن‌ها در ذهن دایره کوچکی از مردم حفظ شده‌اند که رشته فرعی ریاضی خود را از افرادی یاد گرفته‌اند که آن را از فردی که آن را اختراع کرده‌است یاد گرفته‌اند-یعنی تقریبا به صورت فولکلور وجود دارد.
حوزه‌های دیگری نیز وجود دارند که در آن‌ها مواد بنیادی نوشته شده‌اند، اما آن قدر طولانی و پیچیده است که هیچ‌کس نتوانسته بررسی کند که کاملا درست هستند یا نه. در عوض، ریاضی دانان به سادگی به آن‌ها ایمان دارند.
پاتریک مسوت از دانشگاه پاریس سکلی می‌گوید «ما بر شهرت نویسنده تکیه می‌کنیم. ما می‌دانیم که او یک نابغه و فردی محتاط است، بنابراین آنچه گفته باید درست باشد.»
این یکی از دلایل جذابیت زیاد دستیاران اثبات است. تبدیل ریاضیات به یک زبان کامپیوتری می‌تواند ریاضی دانان را مجبور کند تا در نهایت دانش خود را فهرست کرده و اهداف را به دقت تعریف کنند.
آسیه محبوبی، از موسسه تحقیقات ملی فرانسه، اولین باری را به یاد می‌آورد که پتانسیل چنین کتابخانه دیجیتالی منظمی را درک کرده بود: « برای من جالب بود که انسان می‌توانست کل ادبیات ریاضی را با زبان منطقی محض ضبط کند و یک پیکره ریاضی را در کامپیوتر ذخیره کند و با استفاده از این قطعات نرم‌افزار آن را بررسی و مرور کند.»
لین اولین برنامه با این پتانسیل نیست. اولین برنامه، به نام «Automath»، در دهه ۱۹۶۰ بیرون آمد، و Coq، یکی از پر استفاده ترین دستیاران اثبات امروزه، در سال ۱۹۸۹ بیرون آمد. کاربران Coq بسیاری از ریاضیات را به زبان آن رسمی کرده‌اند، اما کار آن‌ها غیر متمرکز و سازمان دهی نشده است. ریاضی دانان روی پروژه‌هایی کار می‌کردند که مورد علاقه آن‌ها بود، تنها موضوعات ریاضی مورد نیاز برای اجرای پروژه‌های خود را تعریف می‌کردند و اغلب آن‌ها را به روش‌های منحصر به فرد توصیف می‌کردند. در نتیجه، کتابخانه‌های Coq مانند یک شهر برنامه‌ریزی نشده هرج و مرج هستند.
محبوبی که به طور گسترده با این برنامه کار کرده‌است گفت: « Coq اکنون یک پیرمرد است و زخم‌های زیادی دارد. بسیاری از افراد در طول زمان بطور مشترک از آن نگهداری کرده‌اند و به دلیل سابقه طولانی آن، نقایصی داشته‌است.»
در سال ۲۰۱۳، یک محقق مایکروسافت به نام لئوناردو دی‌مورا لین را راه‌اندازی کرد. این نام نشان‌دهنده تمایل دومورا به ایجاد برنامه‌ای با یک طراحی کارآمد و منظم است. او این برنامه را به عنوان ابزاری برای بررسی دقت کد نرم‌افزاری در نظر گرفت، نه ریاضی. اما به نظر می‌رسد بررسی درستی نرم‌افزار بسیار شبیه تایید یک اثبات است.
دومورا گفت: « ما لین را ساختیم زیرا به توسعه نرم‌افزار اهمیت می‌دهیم و این قیاس بین ساخت ریاضی و ساخت نرم‌افزار وجود دارد.»
وقتی لین منتشر شد، دستیارهای اثبات زیادی وجود داشتند، از جمله Coq، که بیشتر شبیه به Lean است-پایه‌های منطقی هر دو برنامه براساس تئوری نوع وابسته هستند. اما لین فرصتی برای شروع کار جدید بود.
ریاضی دانان به سرعت به سمت آن کشیده شدند. آن‌ها چنان مشتاقانه از این برنامه استقبال کردند که شروع به صرف زمان دمورا با سوالات توسعه‌ی مخصوص ریاضی خود کردند. موریسون گفت: «او از اینکه مجبور باشد مدیریت ریاضی‌دانان را به عهده بگیرد کمی ناراحت شد و گفت: چطور است که شما خودتان یک منبع جدا بسازید؟»
ریاضی دانان آن کتابخانه را در سال ۲۰۱۷ ساختند. آن‌ها آن را mathlib نامیدند و مشتاقانه آن را با دانش ریاضی جهان پر کردند و آن را به نوعی کتابخانه اسکندریه قرن بیست و یکم تبدیل کردند. ریاضی دانان بخش‌هایی از ریاضیات دیجیتالی شده را ایجاد و آپلود کردند و به تدریج کاتالوگی برای پیشبرد لین ساختند. و از آنجا که mathlib جدید بود، می‌توانستند از محدودیت‌های سیستم‌های قدیمی‌تر مانند Coq یاد بگیرند و توجه بیشتری به چگونگی سازماندهی داشته باشند.
مکبث گفت: « تلاش واقعی برای ساخت کتابخانه‌ای یکپارچه از ریاضیات& که در آن همه قطعات با دیگر قطعات کار می‌کنند، وجود دارد.»
mathlib اسکندریه
صفحه اول mathlib یک داشبورد دارد که در هر لحظه پیشرفت پروژه را نشان می‌دهد. این شرکت دارای یک هیئت مدیره از مشارکت‌کنندگان ارشد است که توسط تعداد خطوط کدی که آن‌ها ایجاد کرده‌اند، رتبه‌بندی شده‌اند. همچنین یک حساب جاری از کل مقدار ریاضیاتی که دیجیتالی شده است وجود دارد: تا اوایل اکتبر، mathlib شامل ۱۸۴۱۶ تعریف و ۳۸،۳۱۵ قضیه است.
اینها عناصری هستند که ریاضی دانان می‌توانند در لین با هم ترکیب کنند تا ریاضیات را بسازند. در حال حاضر، با وجود این ارقام، این برنامه محدود است. لین تقریبا هیچ چیزی از تجزیه و تحلیل پیچیده یا معادلات دیفرانسیل-دو عنصر اساسی بسیاری از زمینه‌های ریاضیات سطح بالاتر-در بر ندارد و حتی به اندازه کافی نمی‌داند که بتواند هیچ یک از مشکلات جایزه هزاره را بیان کند.
اما mathlib کم‌کم در حال پر شدن و تکمیل است. این کار مثل ایجاد یک انبار است. در زولیپ، ریاضی دانان تعاریفی که باید ایجاد شوند را شناسایی می‌کنند، داوطلب می‌شوند که آن‌ها را بنویسند و به سرعت در مورد کار یکدیگر بازخورد ارائه کنند.
مکبث گفت: «هر ریاضیدان تحقیقاتی می‌تواند به mathlib نگاه کند و ۴۰ چیزی که وجود ندارد را شناسایی کند. بنابراین شما تصمیم می‌گیرید که یکی از آن شکاف‌ها را پر کنید. واقعا لذت آنی است. شخص دیگری ظرف ۲۴ ساعت آن را می‌خواند و درباره آن نظر می‌دهد.»
بسیاری از افزوده‌ها کوچک هستند، مثل چیزی که سوفی مورل از مدرسه عالی در لیون در طول کارگاه «لین برای ریاضیدان کنجکاو» در تابستان امسال کشف کرد. سازمان دهندگان کنفرانس به شرکت کنندگان عبارت‌های ریاضی نسبتا ساده‌ای دادند تا به عنوان تمرین در لین اثبات کنند. مورل در حالی که روی یکی از آن‌ها کار می‌کرد، متوجه شد که اثبات او، لما-نوعی نتیجه سنگ‌بنایی-را طلب می‌کند که mathlib نداشت.
«چیز بسیار کوچکی در مورد جبر خطی بود که به نوعی هنوز وجود نداشت. مورل که خودش لمای سه خطی را کدنویسی کرد، گفت: « کسانی که mathlib می‌نویسند سعی می‌کنند کامل باشند، اما شما هرگز نمی‌توانید همه چیز را در نظر بگیرید.»
کمک‌های دیگر بسیار مهم هستند. در سال گذشته، گوزل بر روی تعریف «منیفلد هموار» برای mathlib کار کرده‌است. منیفلدهای هموار فضاهایی هستند-مانند خطوط، دایره‌ها و سطح یک توپ-که نقش اساسی در مطالعه هندسه و توپولوژی دارند. آن‌ها همچنین اغلب در نتایج بزرگ در حوزه‌هایی مانند نظریه اعداد و تحلیل ظاهر می‌شوند. شما بدون تعریف یک تحقیق ریاضی نمی‌توانید امیدوار باشید که بیشتر انواع تحقیقات ریاضی را انجام دهید.
اما منیفلدهای هموار بسته به موضوع، در شکل‌های مختلفی ظاهر می‌شوند. آن‌ها می‌توانند بعد متناهی یا نامتناهی داشته باشند، مرزی داشته باشند یا نداشته باشند و در سیستم‌های عددی مختلفی مانند اعداد حقیقی، مختلط یا p-دوتایی تعریف شوند. تعریف یک منیفولد هموار تقریبا مانند تلاش برای تعریف عشق است: وقتی آن را می‌بینید می‌دانید، اما هر تعریف محکمی احتمالا برخی از نمونه‌های آشکار از این پدیده را مستثنی می‌کند.
گوزل گفت: « برای یک تعریف پایه، شما هیچ انتخابی [ برای نحوه تعریف آن ] ندارید. اما با اشیا پیچیده‌تر، شاید ۱۰ یا ۲۰ راه مختلف برای رسمی کردن آن وجود داشته باشد.»
گوزل مجبور بود بین خاص بودن و عمومی بودن تعادل برقرار کند. او گفت: « قانون من این بود که، من ۱۵ مورد از کاربردهای منیفلدها را می‌دانم که می‌خواستم قادر به بیان آن‌ها باشم. اما نمی‌خواستم تعریف بیش از حد عمومی باشد، چون در این صورت شما نمی‌توانید با آن کار کنید.»
تعریفی که او ارائه داد ۱۶۰۰ خط کد را پر کرد، که برای تعریف mathlib بسیار طولانی است، اما شاید در مقایسه با احتمالات ریاضی که در لین باز می‌کند، ناچیز باشد.
او گفت: « اکنون که ما زبان را داریم، می‌توانیم شروع به اثبات قضایا کنیم.»
پیدا کردن تعریف درست برای یک هدف، در سطح صحیح کلیت، دغدغه اصلی ریاضی‌دانان در ساختن mathlib است. خالقان آن امیدوارند که اهداف را به شیوه‌ای تعریف کنند که در حال حاضر مفید باشد، اما به اندازه کافی انعطاف‌پذیر باشد تا با کاربردهای پیش‌بینی‌نشده ریاضی دانان برای این اشیا تطبیق پیدا کند.
مکبث گفت: « تاکیدی بر مفید بودن هر چیزی در آینده وجود دارد.»
عمل باعث کمال گرایی می‌شود
اما لین تنها مفید نیست-بلکه به ریاضی دانان شانس تعامل با کارشان را به شیوه‌ای جدید می‌دهد. مکبث هنوز اولین باری که یک دستیار اثبات را امتحان کرد را به یاد می‌آورد. سال ۲۰۱۹ و با برنامه Coq بود (گرچه او اکنون از لین استفاده می‌کند). او نمی‌توانست آن را زمین بگذارد.
مکبث گفت: « در یک آخر هفته دیوانه کننده، من ۱۲ ساعت در روز را صرف آن کردم. کاملا اعتیادآور بود.»
ریاضی دانان دیگر نیز در مورد این تجربه به همین شکل صحبت می‌کنند. آن‌ها می‌گویند که کار کردن در لین مانند بازی ویدئویی است-بازی کامل با همان هجوم نوروشیمیایی مبتنی بر پاداش که کنار گذاشتن دسته‌ی بازی را دشوار می‌کند. لیوینگستون گفت: « شما می‌توانید ۱۴ ساعت در روز در آن کار کنید و خسته نشوید و در کل روز احساس خوبی داشته باشید. شما دائما در حال تقویت مثبت هستید.»
با این حال، انجمن لین تشخیص می‌دهد که برای بسیاری از ریاضی دانان، سطوح کافی برای بازی کردن وجود ندارد.
کریستین سزجدی، مهندسی در گوگل که بر روی سیستم‌های هوش مصنوعی کار می‌کند که امیدوار است بتواند به طور خودکار کتاب‌های ریاضی را بخواند و رسمی کند، می‌گوید: « اگر بخواهید بدانید که چه میزان از ریاضیات رسمی شده، من می‌گویم که این کم‌تر از یک هزارم درصد است.»
اما ریاضی دانان درصد را افزایش می‌دهند. در حالی که امروزه mathlib بیشتر محتوا تا سال دوم دوره کارشناسی ریاضی را در بر می‌گیرد، شرکت کنندگان امیدوارند که بقیه برنامه‌درسی را در عرض چند سال اضافه کنند-یک نقطه عطف مهم.
بازارد گفت: «در ۵۰ سال گذشته این سیستم‌ها وجود داشته‌اند، یک نفر هم نگفته بود بیایید بنشینیم و یک بدنه منسجم از ریاضیات را سازماندهی کنیم که نشان‌دهنده آموزش دوره کارشناسی است. ما چیزی می‌سازیم که سوالات امتحان نهایی دوره کارشناسی را درک کند و این کار قبلا هرگز انجام‌نشده است.»
احتمالا چند دهه طول می‌کشد تا mathlib محتوای یک کتابخانه تحقیقاتی واقعی را داشته باشد، اما کاربران لین نشان داده‌اند که حداقل ساخت چنین کاتالوگ جامعی ممکن است-که رسیدن به آن صرفا یک موضوع برنامه‌نویسی در تمام ریاضیات است.
برای رسیدن به این هدف، سال گذشته بازارد، مسوت و یوهان کامملین از دانشگاه فرایبورگ در آلمان یک پروژه اثبات ایده بلند پروازانه را به عهده گرفتند. آن‌ها به طور موقت تجمع تدریجی ریاضیات در دوره کارشناسی را کنار گذاشتند و به خط مقدم این رشته صعود کردند. هدف تعریف یکی از نوآوری‌های بزرگ ریاضیات قرن بیست و یکم بود-چیزی به نام فضای کمال گرا که در دهه گذشته توسط پیتر اسفیز از دانشگاه بن توسعه داده شد. در سال ۲۰۱۸، این کار مدال فیلدز، بالاترین افتخار ریاضی را به دست آورد.
بازارد، مسوت و کامملین امیدوار بودند که نشان دهند که حداقل در اصول، لین می‌تواند به نوعی از ریاضیات که ریاضی دانان واقعا به آن اهمیت می‌دهند، بپردازد. محبوبی گفت: « آن‌ها موارد بسیار پیچیده و جدید را می‌گیرند و نشان می‌دهند که کار بر روی این اهداف با یک دستیار اثبات ممکن است.»
برای تعریف یک فضای کمال گرا، سه ریاضیدان باید بیش از ۳۰۰۰ تعریف از دیگر اهداف ریاضی و ۳۰۰۰۰ ارتباط بین آن‌ها را با هم ترکیب می‌کردند. این تعاریف در بسیاری از حوزه‌های ریاضی از جبر گرفته تا توپولوژی تا هندسه گسترده شده‌اند. روش تجمع آن‌ها در تعریف یک هدف واحد، تصویری واضح از نحوه پیچیده‌تر شدن ریاضیات در طول زمان است-و این که چرا بسیار مهم است که پایه‌های mathlib را به درستی قرار دهیم.
مکبث گفت: « بسیاری از حوزه‌های پیشرفته ریاضی نیازمند هر نوع ریاضی هستند که شما در دوره کارشناسی یاد می‌گیرید.»
این سه نفر موفق به تعریف یک فضای کمال گرا شدند، اما در حال حاضر، ریاضی دانان نمی‌توانند کار زیادی با آن انجام دهند. لین قبل از اینکه بتواند انواع سوالات پیچیده که در آن‌ها فضاهای کمال گرا ظاهر می‌شوند را فرموله کند، نیاز به دسترسی به ریاضیات بسیار بیشتری دارد.
مسوت گفت: « کمی مضحک است که لین می‌داند یک فضای کمال گرا چیست، اما تحلیل پیچیده را بلد نیست.»
بازارد با رسمی کردن فضاهای کمال گرا به عنوان یک «ترفند» موافق است-نوعی از شیرین‌کاری اولیه که تکنولوژی‌های جدید گاهی اوقات برای نشان دادن ارزش خود اجرا می‌کنند. در این مورد، موثر واقع شد.
مساوت گفت: « شما نباید فکر کنید که به خاطر کار ما، هر ریاضیدان در اطراف جهان شروع به استفاده از یک دستیار اثبات کرده‌است، اما من فکر می‌کنم که تعداد کمی از آن‌ها متوجه شدند و سوالات زیادی پرسیدند.»
هنوز زمان زیادی طول می‌کشد تا لین یک بخش واقعی از تحقیقات ریاضی شود. اما این بدان معنا نیست که این برنامه یک داستان علمی-تخیلی است که امروز منتشر می‌شود. ریاضی دانانی که مشغول توسعه آن هستند، کار خود را شبیه به گذاشتن اولین مسیر راه‌آهن می‌دانند-یک شروع ضروری برای یک تلاش مهم، حتی اگر هرگز نتوانند سوار شوند.
مکبث گفت: «لین انقدر جالب خواهد بود که ارزش سرمایه‌گذاری بزرگ امروز را خواهد داشت. من اکنون زمانم را سرمایه‌گذاری می‌کنم تا کسی در آینده بتواند این تجربه شگفت‌انگیز را داشته باشد.»
این متن با استفاده از ربات ترجمه مقالات ریاضی و یادگیری ماشین ترجمه شده و به صورت محدود مورد بازبینی انسانی قرار گرفته است.در نتیجه می‌تواند دارای برخی اشکالات ترجمه باشد.
مطلبی دیگر از این انتشارات
با خیال راحت کفتر پرشی بازی کنید و رضایت مشتریانتون رو به رایچت بسپرید
مطلبی دیگر از این انتشارات
هوش مصنوعی فقط بهترین دوست شما نیست، بلکه آینه‌ای برای روح شماست
مطلبی دیگر از این انتشارات
یک تنش کیهانی جدید: جهان ممکن است خیلی نازک باشد