Pembuktian secara matematis adalah sebuah manifestasi dari logika. Tetapi sejumlah hal menjadi sulit bahkan tidak mungkin dibuktikan secara matematis, kata ilmuwan. "Saya pikir saat ini kita memasuki jaman dimana banyak persamaan matematika yang sangat kompleks sehingga kita tidak tahu apakah mereka benar apa salah", kata Keith Devlin dari Universitas Stanford di California. Sebagai contoh dia menunjuk pada Klasifikasi dari Finite Simple Groups, yang diklaim pembuktiannya pada tahun 1980 yang merupakan kerjasama dari beberapa grup yang berkolaborasi. "Duapuluh lima tahun kemudian, kita masih belum mengetahui apakah hasilnya benar atau tidak. Kita kadang memikirkannya, tetapi tidak pernah ada yang menuliskan pembuktiannya", kata Devlin. Sebagian dari permasalahannya ada pada kode komputer yang digunakan saat ini untuk melakukan pembuktian, kata Thomas Hales, dari Universitas Pittsburgh, Pennyslvania, yang membuat buktinya menjadi jarang dapat diakses, bahkan untuk ahli sekalipun. Tumpukan jeruk Pada tahun 1998 Hales memberikan pembuktian secara komputer tentang persamaan Kepler, teorema yang berasa dari tahun 1611. Hal ini tentang cara paling efisien untuk memasukkan bola-bola kedalam sebuah kotak, dengan sedikit tempat kosong yang tersisa. Sepertinya cara terbaik serupa dengan cara menumpuk buah jeruk di supermarket. Pembuktian Hales terdiri lebih dari 300 halaman dan terdiri dari 40.000 baris kode komputer. Saat dia dan koleganya mengirimkannya ke jurnal untuk publikasi, 12 orang ditugaskan untuk membuktikannya. "Setelah sekitar satu tahun mereka kembali kepada saya dan berkata mereka yakin akan kebenarannya 99%", kata Hales. Tetapi ke-12 orang ini meminta untuk meneruskan evaluasi mereka. Bagaimanapun sedikit keraguan tidaklah berlalu seiring waktu. "Setelah empat tahun mereka kembali kepada saya dan berkata mereka masih yakin 99% akan kebenarannya tetapi mereka berkata mereka kelelahan untuk membuktikannya". Sebagai hasilnya, jurnal ini kemudian menggunakan cara yang tidak biasa dengan mempublikasikan artikel tanpa memperoleh formulir sertifikasi (Annals of Mathematics Vol. 162, p. 1063-1183, 2005). Pengecekan otomatis Walaupun penguji memiliki sejumlah komputer, menurut Devlin "Kami telah menyerahkan sebagian tugas pengujian kepada komputer", yang mencatat beberapa sukses seperti Teorema Empat Warna. Kompleksitas yang makin besar tidaklah masalah "Jika Anda ingin menyelesaikan permasalahan yang membutuhkan komputer dan Anda tidak melakukannya sendiri tentu saja Anda menyerahkannya kepada komputer". Dan Devlin menambahkan bahwa semua keraguan ini menjadikannya lebih manusiawi. Devlin dan Hales saat ini menjadi pembicara pada Asosiasi Amerika untuk Perkembangan Sains di St Louis. | 