Masalah berang-berang yang sibuk, masalah ilmu komputer yang telah berlangsung selama empat puluh tahun, akhirnya diselesaikan oleh sekelompok amatir! Perkembangan terobosan ini tidak hanya mengejutkan civitas akademika, tetapi juga diakui oleh ahli matematika terkenal Terence Tao, dan dipuji sebagai perkembangan terpenting dalam bidang ini sejak tahun 1983. Dengan menggunakan asisten pembuktian Coq, mereka berhasil memverifikasi bahwa nilai bilangan berang-berang kelima yang sibuk BB(5) adalah 47.176.870, menunjukkan potensi besar pembuktian berbantuan perangkat lunak dalam memecahkan masalah matematika yang kompleks, dan juga memberi kita wawasan tentang perilaku mesin Turing dan menghentikan masalah.
Dalam bidang ilmu komputer yang misterius, masalah berusia empat puluh tahun yang disebut masalah berang-berang sibuk baru-baru ini berhasil dipecahkan oleh sekelompok amatir. Prestasi tersebut tak hanya menimbulkan sensasi di dunia akademis, tetapi juga diakui oleh matematikawan ternama Terence Tao yang meneruskan pemberitaannya di media sosial dan menekankan pentingnya asisten pembuktian dalam penelitian matematika.
Ilmuwan komputer Scott Aaronson juga memuji penemuan ini, percaya bahwa ini adalah perkembangan paling penting dalam penelitian fungsi berang-berang yang sibuk sejak tahun 1983. Pencapaian ini menandai pemahaman mendalam tentang batas-batas teori komputasi dan menunjukkan potensi pembuktian berbantuan perangkat lunak dalam memecahkan masalah matematika yang kompleks.
Masalah berang-berang yang sibuk ini bermula lebih dari 40 tahun yang lalu di Dortmund, Jerman, ketika para ilmuwan komputer mencoba menemukan mesin Turing spesifik yang dapat menulis angka 1 terbanyak sebelum berhenti. Mesin Turing adalah model komputasi abstrak yang diusulkan oleh Alan Turing pada tahun 1936 yang melakukan penghitungan pada pita magnetik yang panjangnya tak terhingga dengan membaca dan menulis angka 0 dan 1.
Setelah nomor berang-berang sibuk keempat ditentukan pada tahun 1974, penemuan berang-berang kelima menjadi pertanyaan terbuka. Kini, komunitas online lebih dari 20 kontributor dari seluruh dunia, dengan menggunakan software asisten bukti bernama Coq, telah berhasil memverifikasi bahwa nomor Busy Beaver kelima BB(5) memiliki nilai 47.176.870.
Pencapaian ini tak hanya membuat heboh masyarakat, namun juga menggugah keheranan ilmuwan komputer Damien Woods yang mengibaratkan kemajuan tersebut dengan kecepatan Usain Bolt. Meskipun solusi terhadap masalah ini mungkin tidak dapat diterapkan secara langsung pada bidang ilmu komputer lainnya, bagi para peserta, perjuangan melawan ketidakmungkinan matematis ini merupakan imbalan terbesar.
Inti dari masalah berang-berang sibuk terletak pada pemahaman perilaku mesin Turing, khususnya kinerjanya dalam menghentikan masalah. Perilaku mesin Turing ditentukan oleh seperangkat aturan, yang dapat dibayangkan sebagai sebuah tabel. Setiap aturan menentukan tindakan yang harus dilakukan ketika kepala baca/tulis menemukan angka 0 atau 1 dalam keadaan tertentu.
Meskipun mesin Turing dapat terjebak dalam putaran tak terbatas, menentukan apakah mesin tersebut akan berhenti berjalan adalah masalah yang belum terpecahkan. Matematikawan Tibor Radó tidak puas dengan kesimpulan ini, dan kemudian menciptakan "permainan berang-berang yang sibuk" untuk mengeksplorasi sifat masalah penghentian dengan mengelompokkan mesin Turing berdasarkan jumlah aturan yang mereka miliki.
Peneliti awal, seperti Allen Brady, mengeksplorasi masalah ini dengan menulis program untuk mensimulasikan perilaku mesin Turing. Karyanya dan penemuan peneliti lain meletakkan dasar bagi penjelajah selanjutnya.
Hingga tahun 2022, mahasiswa pascasarjana Tristan Stérin meluncurkan Busy Beaver Challenge, sebuah proyek kolaboratif online yang bertujuan untuk menyelesaikan BB(5). Melalui metode inovatif dan bantuan asisten Coq proof, tim akhirnya berhasil menemukan berang-berang sibuk kelima.
Pencapaian ini bukan hanya tantangan terhadap kemustahilan matematika, namun juga eksplorasi batas-batas ilmu komputer. Dengan dikonfirmasinya BB(5), para peneliti sedang menyusun makalah akademis yang akan menjadi versi yang dapat dibaca manusia yang melengkapi bukti Coq. Pada saat yang sama, mereka juga memikirkan apakah eksplorasi BB(6) akan menjadi target selanjutnya.
Referensi: https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/
Pemecahan masalah berang-berang yang sibuk ini tidak hanya merupakan terobosan besar dalam bidang matematika, namun juga memberikan arahan dan ide baru bagi penelitian teori komputasi masa depan. Pencapaian ini mendorong lebih banyak orang untuk berpartisipasi dalam penelitian matematika dan ilmu komputer serta menjelajahi bidang yang belum diketahui bersama-sama.