مهروماه

امروزه ریاضیات محض وابستگی شدیدی به محاسبات نرم‌‌افزاری پیدا کرده است. حتی برخی از بزرگ‌‌ترین نوابغ این علم نیز این روزها برای درک و اعتبارسنجی اثبات‌‌های خود ناگزیر شده‌‌اند که به نرم‌‌افزارها روی آورند.

کوین بازارد، نظریه‌‌پرداز عددی و استاد ریاضی محض از کالج سلطنتی لندن بر این باور است، زمان آن رسیده که عصر جدیدی در ریاضیات را برمبنای اثبات رایانه‌‌سازی‌‌شده آغاز کنیم. بزرگ‌‌ترین اثبات‌‌های فعلی به‌‌حدی پیچیده هستند که عملا هیچ بشری نمی‌‌تواند جزئیات آن را درک کند؛ چه رسد که بخواهد آن را اعتبارسنجی کند. بازارد از این موضوع نگران است که بسیاری از اثبات‌‌هایی که ما پیش از این، آن‌‌ها را کاملا صحیح می‌‌پنداشتیم، اساسا غلط از آب درآیند. از این رو، ریاضی‌‌دانان به کمک نیاز دارند.

اما «اثبات» چیست؟ اثبات به‌‌معنای نشان‌‌دادن درستی یک گزاره‌‌ی ریاضیاتی است. با یادگیری تکنیک‌‌های جدید اثبات، ما قادر به درک ریاضیات خواهیم شد و نتایج این علم نهایتا در بسیاری از زمینه‌‌های دیگر علمی به‌‌کار گرفته خواهد شد

برای تولید یک اثبات، باید کار را با معانی آغاز کنیم. برای مثال، مجموعه اعداد صحیح را در نظر بگیرید؛ مجموعه‌‌ای متشکل از تمام اعداد صحیح از منفی بی‌‌نهایت تا مثبت بی‌‌نهایت. این مجموعه را به‌‌شکل ...، ۱،۲، ۰، ۱-، ۲-،... بنویسید. سپس نظریه‌‌ای را مطرح کنید؛ برای مثال، بگویید «بزرگ‌ترین عدد صحیح وجود ندارد.» اثبات این نظریه متشکل از یک استدلال منطقی خواهد بود که نشان دهد این نظریه صحیح یا غلط است (که درمورد گزاره‌‌ی اخیر صحیح است). مراحل منطقی در این اثبات هر یک بر مبنای حقایق ازپیش اثبات‌‌شده‌‌ای تعریف خواهد شد که قبلا درستی آن‌ها را پذیرفته‌‌ایم؛ حقایقی از این دست که «عدد یک کوچک‌‌تر از دو است.»

اثبات‌‌های جدید مطرح‌‌شده ازسوی ریاضی‌‌دانان حرفه‌‌ای معمولا بر پایه‌‌ی یک مجموعه نتایج اثبات‌‌شده‌ تعریف می‌‌شوند که پیش‌‌تر درستی آن‌‌ها درک شده است. اما بازارد می‌‌گوید در بسیاری از موارد، حتی درستی اثبات‌‌هایی که اساس اثبات‌‌های بعدی قرار می‌‌گیرند نیز به روشنی درک نمی‌‌شود. برای مثال، مقالات چشمگیری وجود دارند که در آن به نتایج تحقیقاتی ارجاع داده شده که هنوز منتشر نشده‌‌اند. این همان چیزی است که بازارد را نگران کرده است. او در حاشیه‌‌ی دهمین کنفرانس اثبات تعاملی نظریات در پرتلند آمریکا می‌‌گوید:

من ناگهان درمورد درستی بسیاری از نشریات ریاضیاتی احساس نگرانی کردم؛ چراکه ریاضی‌‌دانان معمولا جزئیات را بررسی نمی‌‌کنند و من قبلا نیز غلط‌‌بودن برخی را به چشم دیده‌‌ام.

او در خلال یکی از اسلایدهای ارائه‌‌ی خود در کنفرانس این موضوع را یادآور شده است: «گمان می‌‌کنم شانس اینکه برخی از مهم‌‌ترین کاخ‌‌های ما روی شن بنا شده باشند، صفر نیست؛ هرچند که این شانس کم است.»

ریاضیات مدرن بیش از حد به منابع و اثبات‌های گذشته وابسته شده است
در ریاضیات جدید باید همه‌‌چیز از نو اثبات شود. تمامی مراحل یا دست‌‌کم استدلال‌‌های مطرح‌‌شده باید به‌‌دقت چک شوند. از سوی دیگر، هنوز کارشناسانی زُبده و بزرگانی از جامعه‌‌ی ریاضی حضور دارند که یک راهنمای مطمئن برای اعتبارسنجی گزاره‌‌های صحیح و غلط ارائه کرده‌‌اند. از این رو، اگر یکی از پیش‌گامان علم ریاضی به مقاله‌‌ای ارجاع داده و از نتایج آن در مقاله‌‌ی خود استفاده کرده باشد، پس احتمالا نیازی به بررسی اعتبار اثبات‌‌های مطرح‌‌شده در آن منابع نخواهد بود.

از دیدگاه بازارد، ریاضیات مدرن بیش از حد به منابع گذشته وابسته شده است؛ موضوعی که علت آن به پیچیدگی زیاد نتایج بازمی‌‌گردد. در یک اثبات جدید ممکن است به ۲۰ مقاله‌‌ی قدیمی‌‌تر ارجاع شده باشد و هر یک از این ۲۰ مقاله ممکن است خود دربرگیرنده‌‌ی هزاران صفحه استدلال‌هایی فشرده باشد. در این میان، اگر یک ریاضی‌‌دان مجرب یک مقاله‌‌ی هزار صفحه‌‌ای را بنویسد یا حتی تنها بدان ارجاع کند، ریاضی‌‌دانان دیگر ممکن است تصور کنند که آن مقاله‌‌ی ۱۰۰۰ صفحه‌‌ای (به‌‌همراه اثبات جدید) همگی صحیح هستند و درنتیجه، به خود زحمت بررسی دوباره‌‌ی آن را ندهند. این در حالی است که ریاضیات باید برای همگان قابل‌‌اثبات باشد و نه صرفا برای تعدادی انگشت‌‌شمار کارشناس خبره.

این وابستگی بیش از اندازه‌‌ی ما به مقالات گذشته باعث بروز نوعی شکنندگی در درک حقیقت شده است. برای مثال، اثبات آخرین نظریه‌‌ی فرمات را در نظر بگیرید. این اثبات در سال ۱۶۳۷ ارائه شد و در کتاب رکوردهای جهانی گینس نیز نام آن به‌‌عنوان «دشوارترین مسئله‌‌ی ریاضی» به ثبت رسیده است. بازارد ادعا می‌‌کند که در واقع هیچ‌‌کس به‌‌درستی نتوانسته این اثبات را کاملا درک کند و بدتر اینکه شاید کسی حتی از درستی آن نیز مطمئن نباشد. او می‌‌گوید:

به باور من، هیچ انسانی، زنده یا مرده، جزئیات اثبات نظریه‌‌ی آخر فرمات را نمی‌‌داند؛ با این حال، جامعه درستی آن را پذیرفته است؛ چرا که این اثبات بنابر حکم پیشکسوتان صحیح بوده است.

چند سال پیش، بازارد در خلال گفت‌‌وگویی میان دو تن از زبدگان علم ریاضی با نام‌‌های توماس هالز و ولادیمیر ووسفکی، با مفهوم «اعتبارسنجی نرم‌‌افزاری اثبات» آشنا شد. با کمک چنین نرم‌‌افزاری می‌‌توان اثبات‌‌ها را به‌‌شکلی سیستماتیک و از طریق رایانه اعتبارسنجی کرد. این موضوع می‌‌توانست به‌‌منزله‌‌ی پایانی بر عصر سلطه‌‌ی پیشکسوتان و آغاز دموکراسیزاسیون حقایق علم ریاضی باشد.

این نرم‌افزار اعتبارسنجی اثبات‌‌ها، لین (Lean) نام داشت. بازارد به‌‌محض شروع استفاده از لین، جذب کاربردهای شگفن‌انگیز آن شد. این نرم‌‌افزار نه‌‌تنها باعث شد بازارد بتواند اثبات‌‌ها را بدون هرگونه چون‌‌وچرایی اعتبارسنجی کند؛ بلکه باعث شد یک تفکر شفاف و خلل‌‌ناپذیر درمورد ریاضیات درون وی شکل بگیرد. او می‌‌گوید:

من فهمیدم که رایانه‌‌ها تنها ورودی‌‌هایی با دقت بسیار بالا را قبول می‌‌کنند. این همان روش تفکراتی موردعلاقه‌‌ی من در ریاضیات است. من عاشق آن شدم؛ چراکه حس کردم نیمه‌‌ی گم‌‌شده‌‌ی خود را در آن یافته‌‌ام. من چیزی را یافتم که آن‌گونه درمورد ریاضیات می‌‌اندیشید که خود می‌‌اندیشیدم.

برای آنکه بتوان یک اثبات را به‌‌وسیله‌‌ی لین اعتبارسنجی کرد، کاربر باید آن اثبات را فرمول‌‌بندی کند؛ یعنی آن را از شکل‌‌وشمایل زبان‌‌ها و نمادهای انسانی به زبان برنامه‌‌نویسی لین ترجمه کند. کاربر همچنین باید تمامی تعاریف و اثبات‌‌های جانبی مطرح‌‌شده در آن اثبات را نیز فرمول‌‌بندی کند. ناگفته پیداست که چنین فرایندی وقت و انرژی زیادی می‌‌گیرد؛ با این حال، برتری لین در آن است که می‌‌تواند از پس تمامی گزاره‌‌های ریاضی ورودی برآید؛ موضوعی که درمورد سایر برنامه‌‌های دستیار اثبات صادق نیست.

جامعه‌‌ی روبه رشد ریاضی جهان، به‌‌ویژه در بخش آموزش، از معرفی نرم‌‌افزار لین استقبال کرده است.جرمی اویگاد، استاد علوم نظریه‌‌ی اثبات در دانشگاه کارنگی ملون است. او و بازارد هر دو نرم‌افزار لین را در کلاس‌‌های مقدماتی آموزش اثبات معرفی کرده‌‌اند. نرم‌‌افزار صحت اثبات را خط به خط بررسی می‌‌کند و بازخوردها را نیز گزارش می‌‌دهد. چنین ویژگی‌‌هایی برای دانش‌‌آموزان بسیار مفید واقع خواهد شد.

آویگاد از استقبال جامعه‌‌ی علمی بسیار خشنود به نظر می‌‌رسد، اما هشدار می‌‌دهد که این فناوری هنوز نیاز به توسعه‌‌ی بیش‌‌تری دارد. استفاده از نرم‌‌افزارهای دستیار در اثبات می‌‌تواند بسیار وقت‌‌گیر باشد. او می‌‌گوید با اینکه چیزی حدود چند دهه از معرفی این ایده می‌‌گذرد و پیشرفت‌‌های زیادی نیز حاصل شده است، ولی هنوز به نقطه‌‌ی مطلوب نرسیده‌‌ایم.

بازارد معتقد است که درصورت حل چالش‌‌های پیش رو، نرم‌‌افزار لین می‌‌تواند آثاری فراتر از حوزه‌‌ی اثبات داشته باشد. برای مثال، مشکل جست‌‌وجو را در نظر بگیرید. هر ساله حجم بسیار بالایی از رساله در جهان منتشر می‌‌شود. در چنین آشفته‌‌بازاری، دسترسی به یک روش مناسب برای جست‌‌وجو در میان اثبات‌‌ها بسیار حائر اهمیت خواهد بود. هیلز و بازارد می‌‌گویند که اگر بتوانیم چکیده‌‌ی تمامی مقالات جدید را وارد نرم‌‌افزار کنیم، هر ریاضی‌‌دانی می‌‌تواند با جست‌‌وجو در بانک داده‌‌ی نرم‌‌افزار، هر مقاله‌ای را به‌‌همراه تمامی اطلاعات مربوط به آن بیابد. این به‌‌معنای دسترسی به قدرت بی‌‌نظیر مغز پیشکسوتان ریاضی تنها از طریق یک نرم‌‌افزار خواهد بود.

دانشمندان علوم رایانه می‌‌توانند از این بانک داده‌‌ی عظیم برای آموزش هوش مصنوعی بهره ببرند. از آنجا که نتایج به‌‌دست‌‌آمده از چنین بانک داده‌‌ای به‌‌ زبان خود لین نگاشته شده‌‌اند؛ بنابراین پردازش این نوع اطلاعات برای یک رایانه‌‌ی دیگر نیز بسیار آسان‌‌تر خواهد بود. هدف غایی دانشمندان، تولید یک ماشین خودکار عمومی باهدف اثبات نظریات است؛ نرم‌‌افزای که بتواند اثبات‌‌های مختص‌‌به خود را تولید کند و محاسبات ریاضیاتی را خود انجام دهد. اثبات‌‌کننده‌‌های خودکار به همان فناوری‌‌ای تکیه خواهند داشت که امروزه لین برای اعتبارسنجی اثبات‌‌ها به‌‌کار گرفته است. افزایش مقبولیت نرم‌‌ا‌‌فزاری مانند لین می‌‌تواند نهایتا گامی مؤثر در مسیر اتوماسیون کل ریاضیات به‌‌شمار 

مرکز هلیکس واقع در شمال شرق منهتن قرار است پنجم اکتبر سال جاری میزبان نشستی با موضوع اتوماسیون ریاضیات باشد. در این رویداد که به‌‌صورت زنده ازطریق کانال یوتیوب و وب‌‌سایت آن پوشش داده خواهد شد، مایکل هریس، استاد ریاضی دانشگاه کلمبیا و از همکاران بازارد حضور خواهد داشت.

یکی از دغدغه‌‌های هریس آن است که دانشمندان علوم رایانه و شرکت‌‌های فناوری انگیزه‌‌های یکسانی برای همکاری با ریاضی‌‌دانان در اتوماسیون ریاضی نداشته باشند. برای مثال، دانشمندان علوم رایانه احتمالا تمایل دارند که از فناوری لین برای کسب اطمینان از بی‌‌نقص بودن برنامه‌‌های خود بهره ببرند، شرکت‌‌های فناوری درصدد سودآوری هستند و از آن سو، ریاضی‌‌دانانی نظیر بازارد تنها در اندیشه‌‌ی ارتقاء دانش ریاضیات هستند. هریس می‌‌گوید:

یکی از پیش‌‌بینی‌‌های من این است که اگر افراد نخبه‌‌ای مانند توماس هیلز و بازارد به حرکت خود در این مسیر ادامه دهند، یک نتیجه‌‌ی خارق‌‌العاده در انتظار خواهد بود؛ این نتیجه نه‌‌تنها می‌تواند یک هوش مصنوعی، بلکه شاخه‌‌ای کاملا جدید از ریاضیات یا روشی جدید برای فکرکردن باشد.