Dört Renk Teoremi bilgisayarla kanıtlanan ilk matematik problemi oldu

Matematikçiler Kenneth Appel ve Wolfgang Haken, 1976 yılının Temmuz ayında bir asırdan uzun süredir çözülemeyen Dört Renk Teoremi'ni bilgisayar desteğiyle kanıtladı. Herhangi bir haritadaki komşu bölgelerin aynı renge boyanmaması için en fazla dört rengin yeterli olduğunu savunan teorem, makine gücünden yararlanılarak çözüme kavuşturuldu. Araştırmacılar, karmaşık durumların incelenmesinde 1.200 saatlik işlem süresi ve 10 milyar mantıksal karar kullanan bilgisayar sisteminin, yaratıcılarını aşan zihinsel adımlar sergilediğini açıkladı.

Elde edilen sonuç akademik camiada büyük bir tartışma başlattı. Herbert Wilf ve Paul Halmos gibi isimler, bir insanın baştan sona tek başına doğrulayamayacağı ve akıl yürütme yerine veri doğrulamasına dayanan bu yöntemi gerçek matematikten uzak bularak eleştirdi. Bazı üniversite yöneticileri ise araştırmacıların lisansüstü öğrencilerle buluşmasına dahi izin vermedi. Kanıtın kabul edilebilirliği nesiller arasında da ayrışma yarattı; yaşça büyük matematikçiler bilgisayarlı adımlara şüpheyle yaklaşırken genç araştırmacılar yüzlerce sayfalık elle yapılan hesaplamaları daha riskli gördü.

Tartışmalar sonraki yıllarda felsefi bir boyut kazandı ve 1979 yılında filozof Thomas Tymoczko, incelenemeyen bir kanıtın geleneksel matematik kurallarına uymadığını savundu. Ted Swart gibi matematikçiler ise bilgisayarları kağıt ve kalemin doğal bir uzantısı olarak niteleyip insanların yorulabileceğini ancak makinelerin hata yapmadan çalıştığını belirterek yöntemi savundu. Bill Tutte ve Heinrich Heesch gibi önde gelen uzmanların onayıyla birlikte Dört Renk Teoremi, insan ve makine ortaklığının matematik tarihindeki ilk dönüm noktası olarak kayıtlara geçti.