Matematikawan Terence Tao mengumumkan pengembangan sebuah gim interaktif baru bernama “Lean Grimoire” melalui blog pribadinya, terrytao.wordpress.com. Proyek ini merupakan pembaruan dari buku teks interaktif berbasis JavaScript sebelumnya yang dirilis pada tahun 2018 dengan judul “QED”.
Dari Buku Teks Interaktif Menjadi Gim Pembuktian
Buku teks asli yang pernah diluncurkan tersebut dirancang untuk mengajarkan logika proposisional dan orde pertama melalui format permainan merakit. Pengguna menerapkan berbagai aturan logika guna mencapai kesimpulan yang diinginkan dari sekumpulan hipotesis yang diberikan.
Dengan memanfaatkan agen pengodean modern, Tao merancang ulang permainan tersebut dengan menyematkan sejumlah fitur baru. Salah satu fitur utamanya adalah opsi untuk menampilkan bukti Lean yang sedang berjalan berdasarkan status permainan pemain saat ini.
Fitur Tematik dan Kebutuhan Pengujian
Sebagai tambahan hiburan, permainan ini juga menyediakan mode fantasi. Dalam mode tersebut, elemen-elemen permainan disajikan menggunakan teks bernuansa fantasi, di mana pernyataan matematika berubah menjadi ramalan dan ekspresi matematika berubah menjadi gulungan kertas.
Pengembangan proyek ini bermula dari eksperimen menggunakan agen pengodean untuk membangun aplikasi visualisasi matematika pada bulan Juli. Setelah sempat tertunda akibat berbagai kesibukan, Tao akhirnya dapat merampungkan kembali proyek tersebut. Saat ini, ia membuka kesempatan bagi publik untuk melakukan uji coba permainan guna meningkatkan kegunaannya sebagai sarana pembelajaran pembuktian logis maupun bahasa Lean.
Sumber: Hacker News: Front Page
