مناقشه «اثبـات»

A Philosophical Controversy over "Proof" in Mathematics

حدس چهار رنگ - اينكه براي رنگ كردن هر نقشه جغرافيايي چهار رنگ كافي است - يكي از حدس‌هاي مشهور رياضي است كه بيش از صد سال فكر رياضي‌دانان را به خود مشغول كرده بود. در سال (1976) اثبات كاملي از اين قضيه با استفاده از كامپيوتر‌ها ارايه شد. اين اثبات قابل بررسي، بازبيني و تاييد مستقيم به وسيله يك عامل عقلاني نبود. يعني رياضي‌دانان نمي‌توانستند تك تك مراحل اين اثبات را به وسيله دست و مداد و كاغذ كنترل نمايند. به عبارت ديگر اين اثبات صوري‌پذير بود اما بررسي‌پذير نبود. بنابراين چنين اثباتي يك اثبات به شيوه سنتي در رياضيات نبود. پس آيا اثبات كامپيوتري واقعاً يك اثبات رياضي بود؟ پاسخ‌هاي متفاوت و معارض هم به اين پرسش سبب مناقشه عظيمي درباره مفهوم «اثبات» يعني بنياني‌ترين مفهوم در رياضيات شد و مجموعه‌اي از مسايل عميق فلسفي را بوجود آورد. اما از آنجا كه اثبات‌هاي كامپيوتري خصلتي كم و بيش تجربي به اثبات رياضي مي‌دهند بحران اثبات همچنان ادامه يافت تا سرانجام به تاسيس مجله تخصصي رياضيات تجربي در (1992) انجاميد. اين مقاله سعي دارد با استناد به شواهد تاريخي به بيان پيامد‌هاي فلسفي اين مناقشه در عرصه رياضيات بپردازد.

The Four-Color Conjecture_ that four colors suffice to color every map was a longstanding conjecture well known to every mathematician. It was clearly in the mainstream of mathematics. The year 1976 saw a complete solution to this conjecture. However this proof was essentially dependent on computer. It could not be looked over, reviewed, verified directly by a rational agent. Other mathematicians could not check it by hand. The proof was formalizable but it was not surveyable. This proof is no traditional proof. Is the computer proof really a mathematical proof? The answer to the question leads to serious philosophical problems. Such use of computers in mathematics introduced empirical experiments into mathematics and finally Experimental Mathematics journal published in 1992. The following essay describes the computer proof of the Four-Color Theorem and traces out its philosophical significance.