Dengan menerjemahkan hipotesis Keller ke dalam bahasa pencarian grafik yang dapat dimengerti komputer, para peneliti akhirnya memecahkan masalah menutupi ruang dengan ubin.
Sebuah tim matematikawan akhirnya menemukan hipotesis Keller - tetapi tidak sendiri. Sebaliknya, mereka melatih seluruh armada komputer, dan mereka menyelesaikannya.
Hipotesis Keller, yang diajukan 90 tahun lalu oleh Ott-Heinrich Keller, terkait dengan tugas menutupi ruang dengan ubin identik. Dia berpendapat bahwa jika Anda membuat ruang dua dimensi dengan ubin persegi dua dimensi, setidaknya dua di antaranya harus menyentuh sisi sepenuhnya, dan tidak sebagian. Hipotesis membuat prediksi yang sama untuk setiap dimensi - yaitu, saat mengisi ruang 12 dimensi dengan "persegi" 12 dimensi, setidaknya dua di antaranya harus memiliki sisi yang sama.
Selama bertahun-tahun, ahli matematika memperebutkan hipotesis ini, membuktikan kebenarannya untuk beberapa dimensi dan salah untuk yang lain. Dan pada musim gugur yang lalu, pertanyaan tersebut tetap tidak terpecahkan hanya untuk ruang tujuh dimensi.
Tetapi bukti baru yang dihasilkan komputer memecahkan masalah itu juga. Buktinya , yang diterbitkan Oktober lalu, adalah salah satu contoh terbaru dari kombinasi kejeniusan manusia dan kekuatan komputasi untuk menjawab pertanyaan paling menarik dalam matematika.
Penulis karya baru, Joshua Breukensik dari Stanford, Marin Hijul dan John Mackey dari Carnegie Mellon University, dan David Narvaez dari Rochester Institute of Technology, memecahkan masalah ini dengan menggunakan 40 komputer. Hanya dalam 30 menit, mesin tersebut memberikan jawaban bersuku kata satu: ya, dalam tujuh dimensi, hipotesisnya benar. Dan kita bahkan tidak harus mengambil kesimpulan ini berdasarkan iman.
Terlampir pada jawabannya adalah bukti panjang yang menjelaskan kebenarannya. Buktinya terlalu panjang untuk dipahami manusia, tetapi program komputer lain dapat memverifikasinya.
Dengan kata lain, bahkan jika kita tidak tahu persis apa yang dilakukan komputer untuk membuktikan hipotesis Keller, setidaknya kita dapat memastikan bahwa mereka melakukannya dengan benar.
Dimensi ketujuh yang misterius
Sangat mudah untuk melihat bahwa dugaan Keller benar dalam dua dimensi. Ambil selembar kertas dan coba tutupi dengan kotak yang sama tanpa celah atau tumpang tindih. Anda akan segera menyadari bahwa Anda dapat melakukan ini hanya jika setidaknya dua kotak memiliki sisi yang sama. Jika Anda memiliki kubus di tangan, akan mudah bagi Anda untuk memverifikasi bahwa hipotesis tersebut benar untuk dimensi ketiga. Pada tahun 1930, Keller menyarankan bahwa hubungan ini berlaku untuk semua dimensi dan ubin yang sesuai.
Hasil awal mendukung prediksi Keller. Pada tahun 1940, Oscar Perron membuktikan bahwa hipotesis tersebut benar untuk pengukuran satu sampai enam. Namun, lebih dari 50 tahun kemudian, generasi baru ahli matematika menemukan contoh balasan pertama untuk hipotesis ini: pada tahun 1992, Jeffrey Lagarias dan Peter Shoremembuktikan bahwa hipotesis tidak bekerja dalam dimensi ke-10.
Hipotesis Keller memprediksi bahwa saat mengisi ruang di dimensi mana pun, setidaknya dua ubin harus benar-benar menyentuh sisi.
Saat mengisi ruang dua dimensi, banyak ubin memiliki sisi yang sama (garis biru).
Saat mengisi ruang 3D, banyak kubus memiliki wajah yang sama (biru).
Sangat mudah untuk menunjukkan bahwa jika suatu hipotesis gagal dalam beberapa dimensi, ia tidak berlaku di semua dimensi yang lebih tinggi. Oleh karena itu, setelah pekerjaan Lagarias dan Shor, tinggal menyelesaikan masalah untuk dimensi ketujuh, kedelapan dan kesembilan. Pada tahun 2002, Mackey membuktikan bahwa hipotesis Keller salah untuk dimensi delapan (dan karenanya sembilan).
Hanya dimensi ketujuh yang tetap terbuka - baik itu dimensi terbesar, yang hipotesis ini benar, atau yang terkecil, yang hipotesisnya salah.
“Tidak ada yang tahu persis apa yang terjadi di sana,” kata Khiyul.
Hubungkan titik-titiknya
Sementara matematikawan berjuang dengan masalah ini selama beberapa dekade, metode mereka berangsur-angsur berubah. Perron mengerjakan enam dimensi pertama hanya dengan menggunakan pensil dan kertas, tetapi pada 1990-an para peneliti telah menemukan cara menerjemahkan hipotesis Keller ke dalam bentuk yang sama sekali berbeda - memungkinkan mereka menggunakan komputer untuk menyelesaikannya.
Formulasi asli dari dugaan Keller menyangkut ruang mulus yang berkelanjutan. Dalam ruang seperti itu, ada banyak cara untuk menempatkan ubin dalam jumlah tak terbatas. Tetapi komputer tidak pandai memecahkan masalah dengan jumlah pilihan yang tak terbatas - untuk mengatasinya, mereka membutuhkan objek diskrit dan terbatas.
Marin Hijul dari Universitas Carnegie Mellon
Pada tahun 1990 Kereszteli Korradi dan Sandor Shabo muncul dengan objek diskrit yang sesuai. Mereka menunjukkan bahwa pertanyaan yang setara dengan hipotesis Keller dapat ditanyakan tentang objek ini. Dan jika Anda membuktikan sesuatu yang berkaitan dengan benda-benda tersebut, maka hipotesis Keller akan terbukti. Ini mereduksi soal tak hingga menjadi soal aritmatika yang kurang kompleks dengan bilangan ganda.
Begini cara kerjanya.
Misalkan Anda ingin menangani hipotesis Keller dalam dua dimensi. Corradi dan Shabo menemukan metode untuk ini, menggunakan konstruksi sebuah struktur, yang mereka sebut grafik Keller.
Untuk memulainya, bayangkan ada 16 dadu di atas meja, dan semuanya memiliki tepi atas dengan dua titik (dua titik menunjukkan ruang dua dimensi, dan mengapa ada 16 kubus - kita akan lihat nanti). Semua kubus diputar dengan cara yang sama, sehingga kedua titik tersebut terletak sama untuk setiap orang. Warnai setiap titik dengan salah satu dari empat warna: merah, hijau, putih, atau hitam.
Titik-titik pada satu kubus tidak bertukar tempat - biarkan salah satunya menunjukkan koordinat x, dan yang lainnya - y. Setelah mewarnai kubus, kita mulai menggambar garis, atau tepi, di antara pasangan kubus jika dua kondisi terpenuhi: titik-titik di tempat yang sama untuk sepasang kubus memiliki warna berbeda, dan di tempat lain mereka berbeda dan berpasangan, dan pasangan dianggap merah dengan hijau, atau hitam dengan warna putih.
Grafik Keller untuk dua dimensi. Menemukan himpunan bagian dari empat kubus yang masing-masingnya terhubung satu sama lain, Anda akan membantah hipotesis Keller untuk ruang dua dimensi. Namun, tidak ada bagian seperti itu, dan hipotesisnya benar.
Di bawah ini adalah contoh klik empat dadu yang digabungkan sepenuhnya dan tidak ada dalam grafik.
Artinya, sebagai contoh, jika satu kubus memiliki dua titik merah, dan kubus lainnya memiliki dua titik hitam, mereka tidak terhubung dengan sebuah tepi. Titik-titiknya pada posisi yang sama memiliki warna berbeda, tetapi tidak memenuhi persyaratan warna pasangan. Jika satu kubus memiliki titik merah dan hitam, dan kubus lainnya memiliki dua titik hijau, mereka dihubungkan oleh sebuah tepi, karena di satu posisi mereka memiliki warna berpasangan (merah dan hijau), dan di sisi lain mereka hanya berbeda (hitam dan hijau).
Ada 16 cara mewarnai dua titik dengan empat warna (jadi kita punya 16 kubus). Jelaskan semua 16 kemungkinan ini di depan Anda. Hubungkan semua pasangan kubus yang memenuhi persyaratan. Apakah ada empat kubus dalam skema Anda, yang masing-masing digabungkan dengan tiga lainnya?
Bagian kubus yang terhubung sepenuhnya seperti itu disebut klik. Jika Anda dapat menemukannya, Anda akan menyangkal hipotesis Keller dalam dua dimensi. Namun, Anda tidak bisa - itu tidak ada. Dan ketiadaan klik empat kubus berarti hipotesis Keller benar untuk dua dimensi.
Kubus-kubus ini sebenarnya bukan ubin yang sama dengan hipotesis Keller, namun, Anda dapat berasumsi bahwa setiap kubus mewakili satu ubin. Pertimbangkan warna yang ditetapkan ke titik sebagai koordinat yang menempatkan kubus di ruang angkasa. Dan keberadaan sebuah sisi adalah gambaran bagaimana dua kubus diposisikan relatif satu sama lain.
Jika warna kubus sama, mereka mewakili ubin yang memiliki jarak yang sama dalam ruang. Jika tidak memiliki warna dan pasangan warna yang sama (satu hitam dan putih, yang lain hijau dan merah), ini menunjukkan ubin yang sebagian tumpang tindih - yang tidak diperbolehkan mengisi ruang. Jika dua kubus memiliki satu set warna yang serasi dan satu set dengan warna yang sama (satu merah-hitam, yang lain hijau-hitam), mereka mewakili ubin dengan sisi yang sama.
Akhirnya, dan yang paling penting, jika mereka memiliki satu set warna berpasangan dan satu set warna berbeda - yaitu, jika dihubungkan oleh sebuah tepi - maka kubus mewakili ubin yang bersentuhan satu sama lain, tetapi sedikit bergeser, karena itu tepinya tidak sepenuhnya bertepatan ... Kondisi inilah yang perlu kita pelajari. Kubus yang dihubungkan oleh sebuah tepi menunjukkan ubin yang berdampingan yang tidak memiliki sisi yang sama - ini adalah pengaturan yang diperlukan untuk menyangkal hipotesis Keller.
“Mereka harus bersentuhan, tapi tidak seluruhnya,” kata Khiyul.
Pewarnaan yang sama - pengaturan yang sama.
Warna berbeda, tidak ada pasangan - tumpang tindih.
Dua warna berpasangan dan sepasang warna yang sama adalah sisi yang sama.
Dua warna berpasangan dan dua berbeda - kontak parsial di samping.
Penskalaan
Tiga puluh tahun yang lalu, Corradi dan Shabo membuktikan bahwa ahli matematika dapat menggunakan prosedur serupa untuk bekerja dengan hipotesis Keller dalam dimensi apa pun, dengan mengubah parameter eksperimen. Untuk membuktikan hipotesis Keller dalam tiga dimensi, Anda dapat menggunakan 216 kubus dengan tiga titik di tepinya, dan mungkin tiga pasang warna (namun, ada beberapa fleksibilitas di sini). Maka Anda perlu mencari delapan kubus (2 3 ), yang terhubung sepenuhnya satu sama lain, sesuai dengan kondisi yang sama yang kami berikan di atas.
Secara umum, untuk membuktikan dugaan Keller dalam n dimensi, Anda perlu menggunakan kubus dengan n poin dan mencoba menemukan klik berukuran 2 n di antaranya . Dapat diasumsikan bahwa ini merepresentasikan semacam super-tile (terdiri dari 2 nubin yang lebih kecil) yang mampu menutupi seluruh ruang n-dimensi.
Jika Anda dapat menemukan ubin super ini (yang tidak memiliki ubin dengan sisi yang sama), Anda dapat menggunakan salinannya untuk menutupi seluruh ruang dengan ubin tanpa sisi yang sama, yang akan membantah hipotesis Keller.
“Jika berhasil, Anda dapat menutupi seluruh ruang dengan pemindahan. Sebuah blok tanpa sisi ubin umum akan meluas ke seluruh lantai, ”kata Lagarias, sekarang di University of Michigan.
Mackey menyangkal hipotesis Keller di dimensi ke-8, menemukan klik 256 kubus (2 8 ), sehingga hipotesis tersebut tetap ada di dimensi ke-7, menemukan klik 128 kubus (2 7). Menemukan klik ini akan menyangkal hipotesis Keller dalam dimensi ketujuh. Buktikan bahwa hipotesis itu tidak ada dan Anda akan membuktikan hipotesis itu benar.
Sayangnya, menemukan klik 128 kubus adalah tugas yang sangat sulit. Dalam karya sebelumnya, para peneliti memanfaatkan fakta bahwa dimensi 8 dan 10 dapat, dalam arti tertentu, dapat "diuraikan" menjadi ruang-ruang dengan dimensi yang lebih rendah, yang dengannya lebih mudah untuk dikerjakan. Dan di sini ini tidak berhasil.
“Dimensi ketujuh tidak nyaman karena 7 adalah bilangan prima dan Anda tidak dapat memecahnya menjadi dimensi dengan urutan yang lebih kecil,” kata Lagarias. "Oleh karena itu, tidak ada jalan keluar selain berurusan dengan kombinatorika lengkap dari grafik ini."
Menemukan klik 128 kubus dapat menjadi tantangan bagi otak tanpa bantuan - tetapi ini adalah jenis pertanyaan yang bisa dijawab dengan baik oleh komputer, terutama dengan sedikit bantuan.
Bahasa logika
Untuk mengubah pencarian klik menjadi tugas yang dapat ditangani komputer, Anda perlu merumuskannya dalam istilah logika proposisional . Ini adalah alasan yang logis, yang mencakup sekumpulan batasan.
Katakanlah kalian bertiga sedang merencanakan pesta dengan teman-teman. Anda mencoba membuat daftar tamu, tetapi ada konflik kepentingan. Katakanlah Anda ingin mengundang Alexei atau mengecualikan Kolya. Salah satu teman Anda ingin mengundang Kolya, atau Vlad, atau keduanya. Teman lain tidak ingin menelepon Alexei atau Vlad. Dengan batasan seperti itu, apakah mungkin membuat daftar tamu yang akan memenuhi ketiganya?
Dalam istilah ilmu komputer, masalah ini disebut masalah akseptabilitas. Hal tersebut dapat diselesaikan dengan mendeskripsikan kondisi dalam rumus proposisional. Dalam hal ini, tampilannya seperti berikut, dan A, K, dan B menunjukkan calon tamu: (A OR NOT K) AND (K OR B) AND (NOT A OR NOT B).
Komputer menghitungnya dengan mengganti 0 atau 1 di setiap variabel. 0 adalah nilai variabel "false" atau off, dan 1 adalah "true" atau on. Mengganti 0 bukannya A, kita katakan bahwa Alexei tidak diundang, dan 1 bahwa dia diundang. Dalam rumus sederhana ini, 0 dan 1 dapat diganti (dengan membuat daftar tamu) dengan banyak cara, dan mungkin saja setelah melalui semuanya komputer akan menyimpulkan bahwa tidak mungkin untuk memenuhi semua minat. Namun, dalam kasus ini, ada dua cara untuk mengganti 1 dan 0 untuk menyenangkan semua orang: A = 1, K = 1, B = 0 (undang Alexey dan Kolya) dan A = 0, K = 0, B = 1 (undang satu Vlad ).
Program komputer yang memecahkan pernyataan semacam itu disebut pemecah SAT, di mana SAT adalah kependekan dari kepuasan. Ini memeriksa semua kombinasi variabel dan memberikan jawaban bersuku kata satu - baik YA, ada cara untuk memenuhi persyaratan rumus, atau TIDAK, tidak.
John Mackie dari Universitas Carnegie Mellon
"Anda hanya ingin melihat apakah Anda dapat menetapkan nilai benar dan salah ke semua variabel sehingga seluruh rumus benar, dan jika ya, maka itu memuaskan, dan jika tidak, maka tidak," kata Thomas Hales dari Universitas Pittsburgh.
Pertanyaan untuk menemukan klik dari 128 kubus adalah masalah yang serupa. Ini juga dapat ditulis ulang sebagai rumus proposisional dan diberikan kepada pemecah SAT. Mulailah dengan banyak dadu dengan masing-masing 7 titik dan 6 kemungkinan warna. Apakah mungkin untuk mewarnai titik-titik tersebut sehingga 128 kubus terhubung satu sama lain menurut aturan tertentu? Dengan kata lain, apakah mungkin untuk menetapkan warna agar klik muncul?
Rumus proposisional untuk pertanyaan klik cukup panjang dan mengandung 39.000 variabel. Masing-masing dapat diberi salah satu dari dua nilai, 0 atau 1. Akibatnya, jumlah opsi yang memungkinkan untuk menyusun nilai, atau cara menetapkan warna, adalah 2,39.000 - yang sangat, sangat banyak.
Untuk menemukan jawaban atas pertanyaan tentang hipotesis Keller dalam tujuh dimensi, komputer harus memeriksa semua kombinasi ini - dan mengecualikan semuanya (yang berarti klik ukuran 128 tidak ada, dan hipotesis Keller di dimensi ketujuh benar), atau temukan setidaknya akan menjadi salah satu opsi yang berhasil (menyangkal hipotesis Keller).
"Jika Anda melakukan iterasi sederhana dari semua kemungkinan, Anda menemukan angka 324 digit," kata Mackey. Komputer tercepat di dunia akan berjalan hingga akhir zaman, melewati semua kemungkinan.
Namun, penulis karya baru ini menemukan bagaimana komputer dapat memberikan jawaban pasti tanpa memeriksa semua kemungkinan. Kuncinya adalah efisiensi.
Efisiensi tersembunyi
Mackey mengenang hari ketika, dari sudut pandangnya, proyek itu benar-benar mulai berjalan. Dia berdiri di depan papan tulis di kantornya di Universitas Carnegie Mellon, mendiskusikan masalah tersebut dengan dua rekan penulis, Hijul dan Breikensik, ketika Hijul mengusulkan cara untuk menyusun pencarian sehingga dapat diselesaikan dalam waktu yang wajar.
"Ada manusia jenius yang bekerja di kantor saya hari itu," kata Mackey. - Saya seperti menonton Wayne Gretzky, atau LeBron James di Final NBA. Aku merinding hanya karena mengingatnya. "
Anda dapat menyesuaikan penelusuran untuk grafik Keller tertentu dengan berbagai cara. Bayangkan Anda memiliki banyak kubus di atas meja dan Anda mencoba menyelesaikan 128 kubus, mengikuti aturan Count Keller. Katakanlah Anda telah memilih 12 dengan benar, tetapi Anda tidak tahu cara menambahkan yang berikutnya. Pada titik ini, Anda dapat membuang konfigurasi 128 dadu yang menyertakan konfigurasi 12 yang tidak berfungsi ini.
"Jika Anda tahu lima tugas pertama Anda tidak cocok, Anda tidak perlu mencari variabel lain, dan ini biasanya mengurangi banyak bidang pencarian," kata Shore, sekarang di MIT.
Jenis efisiensi lain dikaitkan dengan simetri. Objek simetris agak sama. Identitas memungkinkan kita untuk memahami keseluruhan objek secara keseluruhan, mempelajari hanya sebagian darinya - melihat setengah dari wajah seseorang, Anda dapat memulihkannya sepenuhnya.
Demikian pula, Anda dapat mengambil jalan pintas dalam kasus grafik Keller. Bayangkan lagi bahwa Anda mencoba untuk menyusun kubus di atas meja. Katakanlah Anda mulai dari tengah tabel dan membangun tangan Anda di sebelah kiri. Anda meletakkan empat dadu dan Anda menemui jalan buntu. Anda sekarang telah menghilangkan satu kombinasi awal dan semua kombinasi berdasarkan itu. Namun, Anda dapat mengecualikan pencerminan kombinasi awal ini - konfigurasi kubus yang Anda dapatkan jika Anda menempatkannya dengan cara yang sama, hanya di sebelah kanan.
"Jika Anda menemukan cara untuk memecahkan masalah yang memuaskan yang dengan cerdik memperhitungkan simetri, Anda telah sangat menyederhanakan tugas," kata Hales.
Empat rekan memanfaatkan efisiensi pencarian ini dengan cara baru - khususnya, mereka mengotomatiskan pertimbangan kasus simetris, sementara ahli matematika sebelumnya memprosesnya hampir dengan tangan.
Hasilnya, mereka meningkatkan pencarian mereka untuk klik berukuran 128 sehingga alih-alih memeriksa 2.39.000 konfigurasi, program mereka hanya memeriksa sekitar satu miliar ( 2,30 ). Ini membuat pencarian yang bisa memakan waktu lama menjadi tugas untuk suatu pagi. Akhirnya, setelah hanya setengah jam perhitungan, mereka menerima jawaban.
"Komputer mengatakan tidak, jadi kami tahu hipotesis itu berhasil," kata Hiyul. Tidaklah mungkin untuk mewarnai 128 kubus sehingga semuanya bergabung satu sama lain, sehingga hipotesis Keller untuk dimensi ketujuh dikonfirmasi. Untuk setiap penempatan ubin yang menutupi suatu ruang, pasti akan ada setidaknya sepasang tepi yang benar-benar bersentuhan.
Komputer tidak hanya memberikan jawaban bersuku kata satu. Dia melampirkan bukti panjang 200 GB yang mendukung kesimpulan ini.
Pembuktian bukan hanya perhitungan dari semua set variabel yang telah diverifikasi oleh komputer. Ini adalah argumen logis yang membuktikan bahwa klik yang diperlukan tidak mungkin ada. Para peneliti memasukkan bukti ke dalam program yang menguji bukti formal dengan menelusuri logika argumen dan memvalidasinya.
“Kami tidak hanya memeriksa semua opsi dan tidak menemukan apa pun. Kami memeriksa semua opsi dan dapat menuliskan bukti bahwa hal seperti itu tidak ada, - kata Mackey. "Kami bisa merekam bukti ketidakpuasan."