خلاصة:
حدس چهار رنگ-اینکه برای رنگ کردن هر نقشه جغرافیایی چهار رنگ کافی است-یکی از حدسهای مشهور ریاضی است که بیش از صد سال فکر ریاضیدانان را به خود مشغول کرده بود.در سال(1976)اثبات کاملی از این قضیه با استفاده از کامپیوترها ارائه شد.این اثبات قابل بررسی،بازبینی و تأیید مستقیم به وسیله یک عامل عقلانی نبود.یعنی ریاضی دانان نمیتوانستند تکتک مراحل این اثبات را به وسیله دست و مداد و کاغذ کنترل نمایند.به عبارت دیگر این اثبات صوریپذیر بود اما بررسیپذیر نبود.بنابراینچنین اثباتی یک اثبات به شیوه سنتی در ریاضیات نبود.پس آیا اثبات کامپیوتری واقعا یک اثبات ریاضی بود؟پاسخهای متفاوت و معارض هم به این پرسش سبب مناقشه عظیمی درباره مفهوم«اثبات»یعنی بنیانیترین مفهوم در ریاضیات شد و مجموعهای از مسائل عمیق فلسفی را بوجود آورد.اما از آنجا که اثباتهای کامپیوتری خصلتی کموبیش تجربی به اثبات ریاضی میدهند بحران اثبات همچنان ادامه یافت تا سرانجام به تأسیس مجله تخصصی ریاضیات تجربی در(1992)انجامید.این مقاله سعی دارد با استناد به شواهد تاریخی به بیان پیامدهای فلسفی این مناقشه در عرصه ریاضیات بپردازد.
ملخص الجهاز:
این پرسش جدا مطرح بود که آیا راهحل اپل و هیکن واقعا اثباتی برای مسئله چهار رنگ است؟آیا این راه حل اساسا یک اثبات ریاضی است؟این پرسشها مناقشات فراوانی را میان ریاضی دانان و فیلسوفان سبب شد به طوری که بنیادیترین مفهوم ریاضیات کلاسیک یعنی«اثبات»را به چالش کشید.
آنها به خوبی میدانستند که کارشان تمام سنت دو هزار ساله ریاضیات را به چالش میکشد بنابراین در مدخل مجله تاکید کردند که«گرچه ما برای روش معمول اثبات قضایا ارزش قائلیم و خود را از نگرش حاکم-که یک نتیجه تنها وقتی به عنوان بخشی از معرفت ریاضی است که به وسیله یک اثبات منطقی حمایت گردد-جدا نمیبینیم اما به نظر ما این غیر عادی است که مؤلفه مهمی از فرایند آفرینش ریاضی از وارد شدن به بحثهای عمومی پنهان مانده است» .
موضوع مورد مناقشه این بود که از زمان یونان باستان تاکنون،اثباتهای ارائه شده در ریاضیات به وسیله ریاضی دانها بررسیپذیر بودهاند اما اثباتهای کامپیوتری این ویژگی را ندارند و تنها دارای خصلت صوریپذیری اثباتها هستند(ویژگی که پس از شکلگیری مکتب صورتگرایی جز خصلتهای لاینفک اثبات قرار گرفته است).
در این صورت آیا باز هم میتوان اثباتهای کامپیوتری را یک اثبات ریاضی دانست؟آیا اصولا احتیاجی هست که اثباتها بررسیپذیر باشند؟ اگر«اثبات»را قلب فعالیت ریاضی بدانیم حل کامپیوتری قضیه چهار رنگ آن را مورد هدف قرار داده است و ازاینرو اعوجاجی جدی و مشکلزا محسوب میشود.
این روش اثبات قضایای ریاضی طرفدارانی در میان ریاضیدانان پیدا کرد و آنان با تأسیس مجله تخصصی(ریاضیات تجربی)، در سال 2991،پایگاهی برای بیان و توسعه فعالیتهای پژوهشی خود ایجاد کردند.