Tim manusia-AI melaporkan pembuktian teka-teki kekacauan berusia puluhan tahun

Matematikawan di Tiongkok melaporkan pembuktian yang telah diperiksa komputer untuk kasus tiga dimensi dari konjektur Ghys, sebuah persoalan yang pertama kali diajukan pada 1995. Tim tersebut menggabungkan pertimbangan ahli dengan model AI untuk mengembangkan argumennya.

Konjektur ini menghubungkan kekacauan dan geometri. Secara umum, pertanyaannya adalah apakah jenis gerak kacau tertentu mengharuskan ruang matematis tempat gerak itu terjadi memiliki struktur yang sangat teratur. Pembuktian yang dilaporkan menyangkut kasus tiga dimensi, bukan menyelesaikan konjektur tersebut secara keseluruhan.

Dipimpin oleh profesor Universitas Great Bay, Xu Disheng, para peneliti bekerja dengan model Shusheng-S2 milik Laboratorium Kecerdasan Buatan Shanghai. Dalam tujuh putaran penalaran, model itu menjelajahi berbagai jalur dan menghasilkan argumen terperinci. Para peneliti mengidentifikasi gagasan yang menjanjikan, menyingkirkan jalur yang menemui jalan buntu, dan mengarahkan putaran eksplorasi berikutnya.

Tim terpisah dari Universitas Peking menerjemahkan empat teorema utama dalam makalah tersebut ke dalam bentuk yang dapat diperiksa komputer. Pembuktiannya lolos pemeriksaan Lean, sistem yang memeriksa penalaran matematis langkah demi langkah. Para ahli juga memastikan bahwa pernyataan formalnya sesuai dengan yang tercantum dalam makalah.

Penelitian ini telah diunggah sebagai pracetak di arXiv, dan kode verifikasinya tersedia untuk umum sehingga pihak lain dapat memeriksa hasil tersebut.