Pemeriksa Bukti dan Kopilot Matematika AI Menurut Terence Tao
(scientificamerican.com)- Seiring pembuktian matematika makin ketat diformalkan, alat seperti Lean mulai memverifikasi bukti manusia dan mengubah landasan kepercayaan dalam kolaborasi berskala besar
- Dengan bertambahnya pustaka standar seperti mathlib, hambatan untuk memformalkan teorema tingkat sarjana hingga bidang baru sedang menurun
- Dalam formalisasi konjektur PFR, lebih dari 20 peserta membagi langkah-langkah pembuktian kecil, sementara Terence Tao berfokus pada pengelolaan arah keseluruhan alih-alih meninjau baris demi baris
- AI saat ini lebih dekat berperan sebagai kopilot pembuktian yang membantu formalisasi, verifikasi, dan pekerjaan repetitif, bukan langsung “menyelesaikan” matematika
- Riset matematika dapat berubah menjadi pekerjaan yang lebih eksplisit dan terbagi, seperti penentuan arah oleh manusia, formalisasi detail, pelatihan AI, dan interpretasi bukti AI
Formalisasi Mengubah Kolaborasi Matematika
- Riset matematika tradisional cenderung berupa kolaborasi kecil, dan Tao biasanya menganggap sekitar 5 orang sebagai batas atas ukuran kolaborasi
- Dengan pemeriksa bukti otomatis (proof checker), kolaborasi dengan ratusan orang yang tidak saling mengenal pun menjadi mungkin
- Kontributor mengunggah kode, lalu Lean compiler memverifikasinya
- Kepercayaan tidak hanya bergantung pada hubungan personal, tetapi dapat dikonfirmasi melalui hasil verifikasi formal
- Saat memformalkan hasil terbaru dari konjektur Polynomial Freiman-Ruzsa(PFR), lebih dari 20 orang ikut berpartisipasi
- Bukti dipecah menjadi banyak langkah kecil
- Setiap peserta menangani pembuktian satu langkah
- Tao mengelola arah kemajuan keseluruhan, alih-alih memeriksa setiap kontribusi baris demi baris
Tidak Semua Matematikawan Perlu Menjadi Programmer
- Dalam proyek formalisasi, pembagian peran dimungkinkan
- Sebagian orang berfokus pada arah matematis
- Sebagian orang secara khusus menangani pekerjaan mengubah potongan kecil matematika menjadi bukti formal
- Matematikawan yang tidak terbiasa dengan komputer, seperti Peter Scholze, juga dapat berpartisipasi dalam proyek Lean
- Jika tugas matematika besar dipecah menjadi potongan-potongan kecil, seseorang dapat berkontribusi pada subtugas tertentu tanpa harus memahami seluruh teori
Kepraktisan yang Dibawa Lean, mathlib, dan Pencarian
- Salah satu alasan besar matematika formal menjadi praktis adalah kemajuan pustaka matematika standar
- Lean memiliki proyek berskala besar bernama mathlib
- Teorema dasar matematika tingkat sarjana seperti kalkulus dan topologi dimasukkan satu per satu ke dalam pustaka
- Tujuannya adalah membawa pustaka tersebut hingga tingkat pascasarjana
- Dengan demikian, memformalkan bidang matematika baru akan menjadi lebih mudah
- Untuk membuat bukti, perlu menemukan teorema yang sudah dikonfirmasi benar, sehingga mesin pencari yang lebih cerdas juga menjadi penting
- Setelah seluruh proyek PFR diformalkan, kompilasi verifikasinya hanya memerlukan sekitar 30 menit
- Hambatannya bukan daya komputasi, melainkan kegunaan, keramahan pengguna, dan adaptasi orang terhadap alat
- Lean saat ini dinilai sebagai bahasa formal dengan komunitas paling aktif
- Untuk proyek penulis tunggal, bahasa lain bisa lebih baik
- Lean mudah dipelajari, serta memiliki pustaka dan komunitas yang baik
- Kelak mungkin digantikan oleh alternatif lain, tetapi saat ini merupakan bahasa formal yang dominan
Biaya Formalisasi Masih Tinggi
- Tao menilai suatu proyek memang dapat diformalkan, tetapi saat ini bisa saja menghabiskan satu bulan waktunya sendiri
- Belum saatnya semua hasil secara rutin diformalkan
- Ketika hal itu membantu mempelajari Lean
- Ketika ada perhatian besar terhadap ketepatan hasil
- Perlu memilih proyek yang formalisasinya memberikan nilai nyata
- Jika teknologinya membaik, biaya formalisasi dapat berkurang
- Saat ini bisa memakan waktu 10 kali lebih lama dibanding cara konvensional
- Ke depan, ada kemungkinan turun menjadi sekitar 2 kali, bahkan kurang dari 1 kali
AI Dapat Menjadi Kopilot Matematikawan
- Tao membayangkan di masa depan matematikawan tidak mengetik bukti secara langsung, melainkan menjelaskannya kepada sistem seperti GPT, sementara AI mencoba melakukan formalisasi Lean selama proses berjalan
- Jika verifikasi lolos, makalah LaTeX dan bukti Lean dapat disediakan bersama
- Jika pengguna menginginkannya, ia dapat menjadi asisten yang membantu hingga pengajuan ke jurnal
- Saat ini, jalur formalisasi tercepat masih ketika manusia lebih dulu membuat ide dan draf bukti
- Dalam jangka panjang, proyek yang memformalkan potongan-potongan kecil tanpa manusia mengetahui keseluruhan bukti, lalu AI dan manusia bersama-sama menghubungkannya untuk membuktikan teorema besar, juga bisa menjadi mungkin
- Tao menilai perlu beberapa tahun hingga cara seperti ini menjadi mungkin
- Teknologi saat ini masih belum cukup, dan formalisasi pun masih merupakan pekerjaan yang menyakitkan
Jarak dari Prospek “Matematika Terselesaikan”
- Tony Wu dan Christian Szegedy pernah mengatakan bahwa dalam 2–3 tahun, matematika akan “terselesaikan” dalam arti mesin akan lebih baik daripada manusia dalam menemukan bukti
- Tao tidak melihat matematika akan terselesaikan, meski dalam 3 tahun AI bisa menjadi berguna bagi matematikawan dan menunjukkan kemajuan yang jelas
- AI dapat menjadi kopilot yang dimintai bantuan ketika satu langkah dalam bukti tampak benar, tetapi manusia tidak langsung melihatnya
- Bahkan jika AI melakukan matematika pada tingkat yang saat ini dilakukan manusia, matematikawan manusia dapat berpindah ke tingkat matematika yang lebih tinggi
- Dengan AI, cara membuktikan ratusan atau ribuan teorema sekaligus juga bisa menjadi mungkin
- Matematikawan manusia berperan mengarahkan apa yang akan dilakukan AI
- Tao menilai proyeksi jadwal 2–3 tahun untuk perubahan seperti ini agak agresif
Memahami Bukti dan Bukti yang Dihasilkan AI
- Bukti matematika bukan sekadar prosedur untuk memastikan kebenaran, tetapi juga proses memahami mengapa sesuatu benar
- Dalam waktu dekat, AI kemungkinan akan lebih dulu mengotomatiskan pekerjaan yang membosankan dan sepele, sementara manusia tetap menentukan arah
- Jika AI menghasilkan bukti yang sulit dipahami dan tampak buruk, manusia dapat menganalisis kembali bukti itu
- Misalnya, pada bukti yang memperoleh kesimpulan dari 10 asumsi, dapat diperiksa apakah bukti tetap berlaku jika satu asumsi dihilangkan
- Jenis matematikawan baru yang mengekstraksi wawasan dari bukti buatan AI dapat muncul
- Bukti AI awal mungkin tampak tidak memiliki wawasan
- Manusia dapat membuat bukti itu lebih dapat dipahami dan menemukan strukturnya
Masalah yang Belum Terpecahkan dan Batasan AI
- Untuk membuktikan konjektur yang belum terpecahkan, pertama-tama perlu memecahnya menjadi potongan-potongan yang lebih kecil
- Mengubah masalah menjadi masalah yang lebih sulit jauh lebih mudah daripada mengubahnya menjadi masalah yang lebih mudah
- Tao menilai AI belum menunjukkan kemampuan bahwa ia lebih baik daripada manusia dalam pekerjaan pemecahan ini
- Penggunaan AI untuk mengusulkan kemungkinan koneksi antarbanyak bidang menarik
- Tingkat keberhasilannya saat ini rendah
- Dari 10 usulan, mungkin hanya 1 yang menarik dan 9 lainnya tidak berguna
- Tao menilai bagian ini bisa berubah di masa depan
Masalah Data dalam Pengetahuan Matematika
- Salah satu masalah dalam pelatihan AI matematika adalah tidak adanya data yang cukup
- Makalah daring dapat digunakan untuk pelatihan, tetapi banyak intuisi matematis tidak terkandung dalam makalah
- Percakapan antarmatematikawan
- Kuliah
- Cara membimbing mahasiswa
- Upaya yang gagal dan proses perbaikannya
- Bukti yang diterbitkan adalah hasil yang sudah dipadatkan, dan orang cenderung hanya menerbitkan kisah sukses
- Data yang benar-benar berharga adalah proses ketika seseorang mencoba sesuatu namun tidak berjalan baik, lalu bagaimana hal itu diperbaiki
- Di masa depan, proses percobaan dan kegagalan riset dapat dicatat dan digunakan untuk pelatihan AI atau untuk mencegah peneliti lain mengulang kegagalan yang sama
- Tao memberi contoh situasi ketika orang setuju merekam proses riset demi memakai sistem seperti AI Lean tingkat lanjut pada 2040
Perubahan Menuju Matematika yang Lebih Eksplisit
- Banyak pengetahuan matematika terkurung di dalam kepala masing-masing matematikawan, dan hanya sebagian sangat kecil yang tersisa secara eksplisit
- Semakin banyak formalisasi, semakin banyak pengetahuan implisit berubah menjadi pengetahuan eksplisit
- Buku teks yang diformalkan dapat berlanjut menjadi buku teks interaktif
- Dimulai dari penjelasan bukti tingkat tinggi
- Langkah yang tidak dipahami dapat dibuka lebih rinci
- Jika diinginkan, pengguna dapat turun hingga tingkat aksioma
- Cara seperti ini dapat membuat matematikawan dari satu bidang lebih mudah berkontribusi ke bidang lain
- Subtugas dari proyek besar dapat ditetapkan dengan tepat
- Seseorang dapat berpartisipasi pada potongan yang diperlukan tanpa memahami keseluruhannya
1 komentar
Opini Hacker News
https://archive.is/Idouw
Ungkapan project manager mathematicians mengingatkan pada tulisan satir Edsger Dijkstra tahun 1975, “A letter to my old friend Jonathan” [1], dan tulisan lanjutannya [2]
Itu adalah tulisan yang mengkritik dengan menunjukkan betapa konyolnya jika cara membuat perangkat lunak diterapkan pada matematika, tetapi dalam beberapa hal terasa visioner
Intinya adalah kritik terhadap absurditas penerapan hak kekayaan intelektual pada pengetahuan, khususnya kebenaran matematis, dan untungnya dalam arus mekanisasi saat ini bagian itu tampaknya bukan kekhawatiran besar
[1]: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD04xx/E...
[2]: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD05xx/E...
Ini tulisan yang berwawasan, tetapi menurut saya bagian yang terlewat adalah bahwa LLM semakin melakukan abstraksi dengan cara yang melampaui manusia
Tao mengatakan “mudah membuat masalah menjadi lebih sulit, tetapi sulit membuatnya menjadi lebih sederhana, dan belum pernah ditunjukkan bahwa AI lebih baik daripada manusia dalam hal ini”, tetapi dari cara kerja LLM, insight pada tingkat yang jauh lebih tinggi bisa saja menjadi mungkin
Saat ini perannya lebih seperti asisten, pemeriksa fakta, dan penangani pekerjaan membosankan, tetapi sebentar lagi ia akan menjadi entitas yang mengusulkan insight. LLM sudah mengompresi embedding dan pengetahuan, serta memiliki insight yang tidak kita lihat
Adegan Hinton memberi contoh keterkaitan antara bom nuklir dan tumpukan kompos: https://www.youtube.com/watch?v=Gg-w_n9NJIE&t=4613s
Ia hanyalah mesin yang dilatih untuk meniru cara manusia menulis, dan tidak ada data pelatihan yang dibutuhkan untuk meniru sesuatu yang lebih pintar daripada manusia
Saya tidak meragukan bahwa machine learning akan melampaui kecerdasan manusia, tetapi bottleneck-nya adalah menemukan cara agar ia belajar sendiri dari keluarannya sendiri tanpa intervensi manusia, alih-alih melakukan regresi atas seluruh tulisan di dunia
Ramanujan tidak memiliki pendidikan formal dan hanya bersentuhan dengan beberapa buku matematika, tetapi tetap menghasilkan penemuan matematis yang brilian; dari sudut pandang data pelatihan model machine learning, itu jumlah yang nyaris tidak ada artinya
Butuh sekitar 10 detik untuk merumuskannya dalam kata-kata, tetapi jika mengetahui informasi yang diperlukan, jawabannya jelas
Hinton mengatakan ini menunjukkan pemikiran analogis, tetapi tulisan terkait berkebun dan pembahasan fisika tumpukan kompos banyak tersedia online, dan ChatGPT kemungkinan sudah melihatnya saat pelatihan
Jadi contoh ini tampak seperti kasus yang gagal mengontrol kemungkinan bahwa LLM pada dasarnya sudah melihat jawabannya dalam teks pelatihan
Bagian setelahnya ketika Ilya mengatakan “ada bukti keberadaan. Otak manusia adalah neural network” (https://youtu.be/Gg-w_n9NJIE?t=4966) juga menarik. Saya pada dasarnya setuju dengan posisi bahwa otak manusia juga neural network, tetapi ada banyak sanggahan bahwa neuron nyata tidak beroperasi dalam 8-bit dan bahwa jenis sel, DNA, serta lingkungan kimia hormonal berbeda, jadi menurut saya ada percabangan filosofis di sini
Itu bisa dilakukan dalam hitungan menit hingga jam
Sebaliknya, untuk mendapatkan satu pakar manusia tambahan, harus ada orang yang menyukai matematika sebagai profesi, melewati pendidikan puluhan tahun dan spesialisasi tingkat lanjut, dan bahkan tidak ada jaminan orang itu akan bertahan sampai akhir serta mencapai tingkat yang mampu mendorong garis depan pengetahuan
Sambil menunggu waktu itu, kita bisa saja membuat triliunan pakar AI yang bekerja secara paralel
Bandwidth otak manusia untuk menyerap informasi baru rendah, tetapi mesin dapat menyalin pengetahuan seumur hidup dalam beberapa detik, menjalankan ribuan percakapan secara paralel, dan bahkan menserialisasi bagian dari otaknya untuk dikirim ke AI lain. Jika sampai pada programmable matter, kita bisa membuat computronium secara eksponensial dan mencapai semacam omega point yang melakukan riset setara ribuan tahun dalam beberapa detik
Saya sama sekali tidak paham matematika, tetapi ini mengingatkan saya pada sejarah software. Dulu, proyek-proyek luar biasa seperti RollerCoaster Tycoon hampir merupakan karya yang dibuat oleh satu orang saja.
Setelah itu, rekayasa software menjadi termodularisasi seperti yang digambarkan dalam wawancara, dan sekarang menjadi lini perakitan raksasa tempat orang seperti saya memproduksi React sebagai mata pencaharian; produktivitas per orang maupun kemampuan yang dibutuhkan rasanya hampir mendekati 0.
Saat sebuah bidang berada di masa jayanya, satu orang jenius bisa menyimpan seratus hal di kepalanya dan menghasilkan karya terbaik; ketika itu digantikan oleh lini perakitan, saya mendapat kesan bahwa bidang tersebut tidak lagi mampu membuat sesuatu yang benar-benar bernilai.
Rekayasa software tidak berhenti melakukan hal-hal keren; menurut saya justru sebaliknya.
Bercanda saja; suatu saat ketika harus memperbaiki bug fatal, kemampuan akan terlihat. Fakta bahwa produk atau layanan sudah stabil dan menguntungkan bukan berarti para developer awal sudah pergi, atau bahwa tidak ada orang yang bisa melakukan hal besar.
Pernyataan bahwa bidang ini tidak lagi membuat sesuatu yang benar-benar bernilai itu sangat keliru.
Rasanya seperti membandingkan katedral yang dibangun 100 orang selama 100 tahun dengan pondok yang dibuat satu orang dalam sebulan. Pondok itu memang berdiri dan bisa menjadi tempat tinggal, tetapi bukan katedral.
Di ranah pengembangan web, bahkan jika hanya ingin melihat Python saja, ada begitu banyak framework dan teknologi untuk setiap roda gigi kecil dalam mesin sehingga benar-benar sulit diikuti.
Kemampuan pada umumnya mengikuti distribusi log-normal, sehingga orang yang luar biasa memang sedikit; bidang kecil pada masa awal kekurangan infrastruktur pendukung, sehingga hanya orang dengan bakat ekstrem yang bertahan, dan kepadatan talenta papan atas bisa menjadi tidak realistis tingginya.
Memaksa merangkai 47 framework terbaru untuk memproduksi aplikasi daftar tugas pada dasarnya berbeda dari menciptakan dampak yang bermakna.
Dari sudut pandang biaya-manfaat, ada optimum lokal yang kuat pada pilihan memuntahkan banyak kode dengan murah ketimbang berinvestasi jangka panjang pada pekerjaan besar; semakin matang sebuah bidang, semakin rendah batas bawah kemampuan yang diperlukan untuk mencapai titik itu.
Tidak banyak organisasi yang berfokus melatih talenta papan atas. Jadi, fenomena rata-rata kemampuan yang menurun begitu saja seiring membesarnya sebuah bidang mudah dijelaskan, dan jika distribusinya ditangani dengan keliru, perbaikannya nanti bisa mahal.
Pembuktian terverifikasi komputer adalah area di mana AI bisa menjadi berguna dalam waktu yang cukup dekat. Namun, bentuknya mungkin lebih mirip neural network pada mesin catur daripada LLM penuh.
Membuktikan semuanya dengan tangan itu membosankan dan memakan waktu, sehingga sudah banyak solver digunakan, tetapi taktik atau solver kesulitan jika diberi terlalu banyak teorema dan lema.
Neural network sebagai mesin pencarian yang menemukan lema terkait lewat pattern matching sangat cocok untuk itu.
Induksi dan unifikasi orde tinggi juga pada dasarnya adalah sintesis kode, dan mengulang secara brute force semua pohon sintaks yang mungkin sangat tidak efisien.
Solver toh melakukan backtracking, jadi tidak masalah jika AI menghasilkan lema yang 95% tidak berguna, dan ini bisa jauh lebih baik daripada pencarian manual.
Namun, saya tidak yakin pembuktian terverifikasi komputer selalu baik untuk komunikasi. Bukti yang dibaca manusia berada pada level tinggi dan menghilangkan detail bukan hanya karena masalah panjangnya.
Masalah intinya adalah ia harus terhubung dengan definisi formal dari objek matematika yang digunakan dalam bukti.
Namun, manusia tidak berpikir seperti itu saat menulis atau membaca bukti. Biasanya mereka punya intuisi informal tingkat tinggi tentang apa yang secara “moral” sedang mereka lakukan, lalu mengisi detail formal seperlunya.
Kode komputer bisa bekerja sampai batas tertentu karena semantik formal bahasa jauh lebih dekat dengan model mental, tetapi dalam matematika tujuannya umumnya berbeda.
Strategi sledgehammer di Isabelle menggabungkan pembukti teorema otomatis seperti E, Z3, SPASS, dan Vampire untuk mencoba membuktikan atau membantah sebuah target.
Secara teori terlihat bagus, tetapi dalam praktiknya sering muncul bukti rekonstruksi yang menerapkan sekitar 12 lema yang tampak acak, dan bukti seperti ini tidak terbaca serta sangat rapuh.
AI tampaknya tidak akan menyelesaikan masalah ini secara ajaib.
Saat ini neural network sangat rendah efisiensi sampelnya, dan dataset matematika formal jauh lebih kecil daripada dataset seperti kode Python.
Terence Tao memberikan ceramah yang sangat bagus tentang topik ini beberapa bulan lalu, dan membahas penggunaan Lean secara lebih rinci: https://www.youtube.com/watch?v=AayZuuDDKP0
Seorang matematikawan aktif mengatakan bahwa dalam penelitiannya ia membuat GPT-4o membuktikan beberapa lema yang kemungkinan baru
“Pasangan saya adalah matematikawan, dan minggu lalu untuk pertama kalinya ia memakai ChatGPT untuk mencoba membuktikan beberapa lema untuk riset. Ia sudah menduga teorema-teorema itu benar dan kira-kira punya pendekatan, tetapi bukan pakar untuk jenis proposisi seperti itu. Ini pertama kalinya ia mendapat bukti yang benar dan berguna dari model
Lema pertama ditemukan seorang kolaborator dari perhitungan untuk nilai e kecil. ChatGPT tidak bisa menemukan bukti sebelum diberi tahu untuk mencoba memakai fungsi Möbius
https://chatgpt.com/share/9ee33e31-7cec-4847-92e4-eebb48d4ff...
Yang kedua terlihat lebih standar dan tampaknya Mathematica juga bisa melakukannya. Namun Mathematica tidak memberi penurunan yang rapi, jadi tetap berguna
https://chatgpt.com/share/7335f11d-f7c0-4093-a761-1090a21579...”
Hal-hal seperti ini menjadi menakutkan bagus dalam penalaran dan topik berat
Jika bidang machine learning terus berfokus menambahkan kemampuan Sistem 2 untuk melengkapi pemikiran Sistem 1 yang kira-kira dimiliki LLM, situasinya tampaknya akan menjadi liar
Itu ingatan yang mengesankan, bukan penalaran baru
Kami memikirkannya sebagai jumlah atas partisi berurutan, bukan jumlah partisi dengan koefisien |τ|!, tetapi keduanya tentu saja sama
Jika memakai partisi yang berurutan secara siklik, yaitu koefisien (|τ|-1)! alih-alih |τ|!, hasilnya 0, bukan (-1)^e
Bukti kombinatorial Beren memilih satu elemen khusus; jika elemen itu sendirian, ia digabung dengan bagian berikutnya, dan jika tidak sendirian, ia dipecah menjadi bagiannya sendiri. Dengan cara ini dibuat bijeksi antara partisi berurutan siklik dengan panjang genap dan ganjil
Untuk urutan linear, terapkan hal serupa mulai dari elemen terakhir, tetapi partisi yang elemen terakhirnya sendirian di bagian terakhir tidak terpasangkan, sehingga lanjut secara rekursif ke elemen berikutnya
Pada akhirnya semuanya terpasangkan, dan yang tersisa hanya partisi dengan semua elemen terpisah serta dalam urutan asal. Jumlah bertanda menurut paritas ukuran himpunan asal menghasilkan proposisi semula
Saya juga tidak tahu ada berapa suku dalam penjumlahan untuk “τ ≤ τ”, dan itu pun tidak cocok dengan bagaimana hal ini terkait dengan membangun salah satu sisi kiri atau kanan pada nomor 3 lalu menyimpulkan sisi lainnya
Sebenarnya ChatGPT mengingat fungsi Möbius dari kisi partisi lalu mengulanginya tanpa bukti, setelah itu mengeluarkan omong kosong yang hanya tampak masuk akal
Membangun fungsi Möbius itu pada dasarnya inti persoalannya, dan pertanyaannya hampir sama dengan meminta pembuktian bahwa fungsi itu berbentuk demikian
Selain itu, rumus umum yang diberikan ChatGPT juga sedikit keliru, dan hanya benar pada kasus |σ| = 1 yang penting untuk bukti saat ini
Fakta ini dapat langsung dilihat tanpa secara eksplisit memakai seluruh perangkat fungsi Möbius, dengan menetapkan N(t,e) sebagai jumlah partisi yang membagi menjadi t kelas ekivalensi, lalu melakukan induksi elementer menggunakan relasi rekuren N(t,e+1)=N(t-1,e)+tN(t,e)
Ada tiga hal yang menonjol dalam wawancara ini
Pertama, Tao membicarakan project manager mathematicians, membayangkan masa depan ketika wawasan matematika juga “diproduksi” seperti keluaran lain dalam masyarakat. Ia melihat alasan matematika belum terindustrialisasi seperti itu sebagai kurangnya alat, dan menganggap AI serta proof assistant bisa revolusioner di bagian ini. Namun interaksi dan arahan manusia tetap diperlukan
Kedua, ada sangat banyak pengetahuan tacit yang tidak termuat dalam makalah. Hal-hal seperti intuisi atau pengetahuan tentang kegagalan itu penting, sehingga bahkan matematikawan terbaik pun harus saling berbicara agar tidak mengulangi kesalahan yang sama
Ketiga, mudah mengira matematika sudah cukup terformalisasi, tetapi dalam makalah banyak pengetahuan bersama yang diasumsikan. Memformalkan bukti dengan cara yang dapat dipahami proof assistant membantu lebih banyak orang memahami apa yang sebenarnya terjadi
Seperti yang ditunjukkan Tao dalam ceramah proyek Polymath, tampak bahwa ia selalu merupakan orang yang mencari cara baru dalam riset matematika
Untuk saat ini, ini mungkin proyek yang memungkinkan ketika peraih Medali Fields seperti Tao atau Scholze punya kelonggaran menghabiskan 10 kali lebih banyak waktu untuk pembuktian
Baru-baru ini saya berbicara dengan seorang postdoc di departemen matematika papan atas, dan ia mengatakan tidak ada orang di sekitarnya yang memakai lean4 dalam pekerjaan nyata
Untuk peneliti tahap awal karier, mungkin lebih baik mempercayai intuisi dan menerbitkan makalah
Untuk melihat topik ini dengan benar, kesan dari beberapa orang saja tidak cukup
Sebaliknya, di bidang dengan gaya lebih intuitif seperti topologi dimensi rendah, saya memperkirakan lebih sedikit orang yang memakai proof checker
Di sini, kata intuitif bukan berarti kurang ketat. Bukti bergambar untuk suatu ekuivalensi homotopi jauh lebih sulit dipindahkan agar bisa dipahami Lean dibandingkan daftar pertidaksamaan
Sebagai catatan, saya berada di bidang geometri/topologi, dan belum pernah melihat atau mendengar ada orang yang memakai alat seperti ini
https://lean-lang.org/
https://github.com/leanprover/lean4
Bagian yang mengatakan, “Jika AI memberikan bukti yang tidak dapat dipahami dan buruk rupa, kita bisa menganalisisnya. Jika bukti ini menggunakan 10 asumsi untuk mendapatkan satu kesimpulan, apakah bukti itu tetap berfungsi jika satu asumsi dihapus? Ilmu semacam ini belum ada karena belum banyak bukti yang dihasilkan AI, tetapi akan muncul jenis matematikawan baru yang menerima matematika hasil AI dan membuatnya lebih mudah dipahami,” persis sama dengan pemikiran saya tentang desain API publik dalam kode
Peran yang secara tradisional hanya dilakukan oleh developer berpengalaman kini bisa sangat disederhanakan dan menjadi dapat diakses oleh semua orang