Soal matematika berumur 400 tahun dipecahkan oleh komputer

Ketika berurusan dengan matematika, hal-hal yang kelihatannya sepele pun bisa menjadi topik yang menarik dan membingungkan. Begitu juga ketika Johannes Kepler menyatakan bila cara terbaik menyusun bola adalah dengan
menumpuknya mirip piramida, banyak sekali yang meragukan teorinya.
Namun, kini pernyataan Kepler yang telah berumur 400 tahun itu terbukti benar berkat bantuan sebuah komputer dan dua buah piranti lunak untuk verifikasi data, Isabelle dan HOL Light. Kedua software tersebut bertugas memastikan apakah cara paling efisien untuk menyusun benda berbentuk lingkaran seperti jeruk adalah dengan tumpukan piramida.
Isabelle dan HOL Light harus memeriksa 300 lembar bukti-bukti pembenaran teori Kepler yang dibuat oleh Thomas Hales dari Universitas Pittsburgh, Amerika, pada tahun 1998 yang lalu. Sebelumnya, Hales harus meminta 12 ahli untuk memeriksa jawabannya atas teori 'piramida jeruk' Kepler.
Hingga pada hari Minggu kemarin (10/08/14), tim Hales berhasil membuktikan kebenaran teori Kepler dengan keyakinan hingga 100 persen berkat verifikasi dari Isabelle dan HOL Light. Padahal, 12 orang ahli matematika sebelumnya hanya bisa memastikan kebenaran dari jawaban Hales di prosentase 99 persen saja, Gizmodo (12/08).
Tak ayal, kabar gembira ini diharap segera bisa menular ke misteri-misteri lain di dunia matematika. Mengingat tiap tahunnya selalu muncul bukti matematika baru yang jumlahnya mencapai jumlah ratusan.
Namun, para pakar matematika nampaknya harus sedikit bersabar saat menggunakan Isabelle dan HOL Light. Sebab, dua software yang digunakan Hales itu membutuhkan waktu bertahun-tahun (terhitung sejak 2003) hanya untuk membuktikan kebenaran satu soal matematika piramida jeruk.
Sumber: Merdeka.com