استفاده از رایانهها برای پایان دادن به یکی از بزرگترین مناقشات ریاضی
به گزارش خبرنگار پژوهندگان عصر ،این مقاله به مناقشه طولانی بر سر «حدس abc» میپردازد؛ یک مسئله عمیق در نظریه اعداد که اعداد اول را به حساب ساده مرتبط میکند. در سال ۲۰۱۲، ریاضیدان ژاپنی، شینیچی موچیزوکی، ادعا کرد که این حدس را در یک اثبات ۵۰۰ صفحهای حل کرده است. با این حال، به دلیل پیچیدگی فوقالعاده و استفاده از مفاهیم کاملاً جدید، جامعه ریاضی هرگز نتوانست صحت آن را به طور کامل تأیید کند و این موضوع به یک دهه بحث و اختلاف نظر دامن زده است.
برای حل این مناقشه، اکنون دو تن از برجستهترین ریاضیدانان جهان به رایانهها روی آوردهاند. کوین بازارد از کالج سلطنتی لندن، در حال رهبری پروژهای برای ترجمه اثبات موچیزوکی به زبان یک نرمافزار «دستیار اثبات» (Proof Assistant) به نام «Lean» است. این نرمافزارها میتوانند صحت یک استدلال ریاضی را قدم به قدم و با دقتی فراتر از توانایی انسان بررسی کنند. در این پروژه، پیتر شولز، یکی از برندگان مدال فیلدز و از منتقدان اصلی کار موچیزوکی، نیز مشارکت دارد. هدف این است که با تبدیل اثبات به کدی قابل فهم برای ماشین، مشخص شود که آیا استدلال موچیزوکی صحیح است یا دارای نقصی پنهان میباشد.
این پروژه نهتنها میتواند به این مناقشه خاص پایان دهد، بلکه نشاندهنده یک تغییر بزرگ در دنیای ریاضیات است. به نظر میرسد ریاضیدانان برای حل مسائل بسیار پیچیده آینده، بیش از پیش به رایانهها برای تأیید صحت اثباتهای خود وابسته خواهند شد. این تلاش، آزمونی برای سنجش رابطه میان شهود انسانی و دقت ماشینی است. اگر کامپیوتر بتواند اثبات موچیزوکی را تأیید کند، این یک پیروزی بزرگ برای او خواهد بود. در غیر این صورت، نشان میدهد که حتی ذهنهای بزرگ نیز ممکن است در پیچیدگیهای استدلالهای خود گم شوند و اینجاست که رایانهها میتوانند به عنوان یک ابزار داوری بیطرف عمل کنند.