Komunitas kecil ahli matematika menggunakan Lean untuk membangun basis digital baru. Mereka berharap ini akan mengamankan masa depan bidang ilmiah mereka.
Setiap hari, lusinan ahli matematika yang berpikiran sama bertemu di obrolan Zulip untuk mengerjakan apa yang mereka yakini akan membentuk masa depan bidang ilmiah mereka.
Mereka semua adalah penggemar program Lean . Ini adalah alat pembuktian teorema interaktif yang, pada prinsipnya, mampu membantu ahli matematika menulis bukti. Namun, untuk ini, ahli matematika harus memasukkan aturan matematika secara manual ke dalam basis program, membawa pengetahuan yang dikumpulkan selama ribuan tahun ke dalam bentuk yang dapat dipahami oleh komputer.
Bagi banyak peserta dalam proyek, manfaatnya membutuhkan sedikit atau tanpa penjelasan.
“Pada tingkat fundamental, jelas sekali bahwa sesuatu telah didigitalisasi, itu dapat digunakan dengan cara baru,” kata Kevin Buzzarddari Imperial College London. "Dan kami akan mendigitalkan matematika, membuatnya lebih baik."
Digitalisasi matematika adalah mimpi lama. Manfaat yang diharapkan dari ini berkisar dari hal sepele - memeriksa pekerjaan rumah siswa dengan komputer - hingga yang luar biasa: menggunakan kecerdasan buatan untuk membuat penemuan matematika baru dan menemukan solusi baru untuk masalah lama. Matematikawan percaya bahwa penguji teorema otomatis juga akan dapat meninjau artikel yang dikirimkan ke jurnal, menemukan kesalahan yang terkadang terlewatkan oleh peninjau manusia, dan terlibat dalam pekerjaan teknis yang membosankan untuk mengisi bukti dengan semua detail yang diperlukan.
Tapi pertama-tama, matematikawan yang bertemu dalam obrolan perlu membekali Lean dengan pengetahuan dalam kerangka matematika sekolah, dan sejauh ini tugas ini baru setengah selesai. Dalam waktu dekat, Lean tidak mungkin dapat memecahkan masalah terbuka, tetapi orang yang bekerja di pangkalan hampir yakin bahwa hanya dalam beberapa tahun program ini setidaknya akan belajar memahami masalah tingkat ujian di sekolah menengah.
Siapa tahu? Matematikawan yang berpartisipasi dalam proyek ini tidak selalu memiliki gagasan yang jelas tentang apa kegunaan matematika digital.
“Kami tidak tahu pasti kemana tujuan kami,” kata Sebastien Gösel dari Universitas Rennes.
Anda merencanakan, Lean bekerja
Selama musim panas, sekelompok pengguna Lean berpengalaman mengadakan seminar online " Lean for Curious Mathematicians ". Dalam pelajaran pertama, Scott Morrison dari University of Sydney menunjukkan bagaimana Anda dapat menulis bukti menggunakan program.
Dia mulai dengan menuliskan pernyataan yang ingin dia buktikan dalam istilah Lean. Dalam bahasa manusia, itu berarti "ada bilangan prima yang tak terbatas." Ada beberapa cara untuk membuktikan klaim ini, tetapi Morrison ingin menggunakan versi yang sedikit dimodifikasi dari bukti pertama yang ditemukan oleh Euclid dari 300 SM. Dalam pembuktiannya, semua bilangan prima yang diketahui dikalikan, dan kemudian, setelah menambahkan 1, diperoleh bilangan prima baru (baik hasil perkaliannya atau salah satu pembaginya akan menjadi bilangan prima). Pilihan Morrison didasarkan pada salah satu aturan dasar untuk menggunakan Lean: pengguna harus menemukan ide utama pembuktian itu sendiri.
"Anda bertanggung jawab atas tebakan pertama," kata Morrison dalam sebuah wawancara.
Setelah memasukkan pernyataan dan memilih strategi, Morrison menguraikan struktur pembuktian dalam beberapa menit. Dia mengidentifikasi urutan langkah-langkah perantara, yang masing-masing relatif mudah dibuktikan. Meskipun Lean tidak dapat menawarkan strategi pembuktian umum, ini dapat membantu Anda menjalankan langkah-langkah kecil dan konkret. Memecah bukti menjadi beberapa tugas yang dapat diakses, Morrison mirip seperti koki yang menginstruksikan koki biasa untuk memotong bawang atau merebus air. "Di sinilah Anda berharap Lean akan mengambil alih dan mulai membantu Anda," kata Morrison.
Lean menyelesaikan tugas menengah menggunakan proses otomatis yang disebut taktik. Ini adalah jenis algoritme singkat yang dirancang untuk melakukan tugas yang sangat spesifik.
Bekerja dengan bukti, Morrison meluncurkan taktik yang disebut pencarian perpustakaan. Dia menyisir database matematika program dan mengembalikan beberapa teorema yang menurutnya dapat mengisi celah di bagian tertentu dari pembuktian. Taktik yang berbeda melakukan tugas matematika yang berbeda. Salah satunya, linarith, dapat mengambil satu set pertidaksamaan untuk, katakanlah, dua bilangan real, dan mengkonfirmasi kebenaran dari pertidaksamaan baru, yang mencakup bilangan ketiga: jika a adalah 2 dan b lebih besar dari a, maka 3a + 4b lebih besar dari 12. Yang lain melakukan sebagian besar bekerja dengan aturan aljabar dasar seperti asosiatif.
“Dua tahun lalu di Lean, asosiatif harus diterapkan secara manual,” kata Amelia Livingston, seorang siswa matematika di Imperial College London yang belajar Lean dengan Buzzard. - Dan kemudian seseorang menulis taktik yang melakukannya untuk Anda. Saya senang setiap kali saya menggunakannya. "
Secara keseluruhan, Morrison butuh waktu 20 menit untuk melengkapi bukti Euclid. Di sana-sini dia menyelesaikan sendiri detailnya; terkadang ahli taktik melakukannya untuknya. Setelah setiap langkah, Lean memeriksa konsistensi bukti sesuai dengan aturan logis bawaan yang ditulis dalam bahasa formal yang disebut teori tipe dependen .
“Sepertinya aplikasi Sudoku. Jika Anda salah langkah, itu akan berbunyi bip, ”kata Buzzard. Akibatnya, Lean mengonfirmasi kelayakan bukti Morrison.
Itu adalah latihan yang sangat menyenangkan - seperti yang biasanya terjadi ketika teknologi melakukan sesuatu untuk Anda. Namun, bukti Euclid telah ada selama lebih dari 2000 tahun. Pertanyaan matematikawan masa kini begitu kompleks sehingga Lean masih belum dapat memahami pertanyaannya, apalagi membantu menjawabnya.
“Mungkin perlu waktu puluhan tahun untuk alat ini membantu penelitian,” kata Heather Macbeth dari Universitas Fordham, salah satu pengguna Lean.
Jadi, sebelum ahli matematika dapat menggunakan Lean pada pertanyaan yang sangat menarik bagi mereka, mereka harus menambahkan lebih banyak aturan matematika ke dalam program. Dan ini sebenarnya adalah tugas yang cukup sederhana.
Anatomi program pembangunan bukti: Lean membantu ahli matematika membuktikan teorema dengan memverifikasi pekerjaan dan mengotomatiskan beberapa langkah dalam pembuktian.
1) Ahli matematika menjelaskan struktur dasar pembuktian, dan menuliskan urutan langkah-langkah di Lean.
2) Perpustakaan program matematika mathlib memiliki seperangkat taktik yang melakukan langkah-langkah pembuktian ini. Matematikawan terus menambahkan data baru ke mathlib. Teorema yang telah terbukti ditambahkan ke mathlib.
3) Algoritma Kernel memeriksa kebenaran bukti menggunakan aturan sederhana.
* Gurita entah bagaimana telah menjadi sebutan untuk emosi gembira di komunitas Lean.
“Agar Lean dapat memahami sesuatu, orang perlu menerjemahkan buku teks matematika ke dalam bentuk yang dapat dipahami oleh program,” kata Morrison.
Sayangnya, kesederhanaan sebuah soal tidak berarti mudah untuk diselesaikan - mengingat sebagian besar soal matematika tidak tercakup dalam buku teks.
Pengetahuan yang tersebar
Jika Anda belum mempelajari matematika tingkat lanjut, bidang ini mungkin tampak akurat dan dijelaskan dengan baik bagi Anda. Aljabar, kalkulus diferensial, analisis matematika - semuanya mengikuti dari semuanya, dan ada jawaban untuk semua pertanyaan, tercantum di akhir buku teks.
Akan tetapi, matematika dalam kurikulum sekolah, kurikulum perguruan tinggi, dan bahkan sebagian besar universitas adalah bagian kecil dari semua pengetahuan. Kebanyakan dari mereka tidak terorganisir dengan baik.
Ada bidang matematika yang sangat besar dan penting yang tidak sepenuhnya dijelaskan. Mereka disimpan di kepala sejumlah kecil orang yang mempelajari sub-bidang matematika mereka dari orang-orang, mempelajarinya dari mereka yang menciptakannya - yaitu, mereka ada berdasarkan cerita rakyat.
Ada area lain di mana bahan dasar telah ditulis, tetapi sangat rumit dan panjang sehingga belum ada yang dapat memverifikasi kebenarannya. Sebaliknya, para ahli matematika hanya mempercayainya.
“Kami mengandalkan reputasi penulis. Kami tahu bahwa dia adalah seorang jenius dan orang yang teliti, jadi buktinya kemungkinan besar benar, ”kata Patrick Massot dari Universitas Paris-Saclay.
Inilah salah satu alasan mengapa program pembuktian teorema begitu menarik. Menerjemahkan matematika ke dalam bahasa yang dapat dimengerti oleh komputer memaksa ahli matematika untuk akhirnya membuat katalog pengetahuan mereka dan secara tepat mendefinisikan semua objek.
Assia Mabubidari French State Institute for Research in Informatics and Automation mengenang saat pertama kali dia menyadari potensi perpustakaan digital yang begitu teratur: "Saya terpikat oleh kemungkinan cakupan teoretis dari semua literatur matematika menggunakan bahasa logika murni, menyimpan seluruh perpustakaan matematika di komputer, memeriksa dan mencari data di dalamnya dengan bantuan program ".
Lean bukanlah program pertama yang memiliki potensi ini. Yang pertama, Automath, muncul pada 1960-an, dan Coq, salah satu yang paling populer saat ini, keluar pada 1989. Pengguna Coq memformalkan banyak matematika dalam bahasa program, tetapi pekerjaan ini terdesentralisasi dan tidak terorganisir dengan baik. Matematikawan bekerja hanya pada proyek yang menarik bagi mereka, dan mengidentifikasi hanya objek yang mereka butuhkan untuk pekerjaan mereka sendiri, seringkali mendeskripsikannya dengan cara yang unik. Akibatnya, perpustakaan Coq tampak berantakan, seperti cetak biru kota yang tumbuh secara alami.
“Coq adalah orang tua dengan bekas luka hari ini,” kata Mabubi, yang aktif dengan program tersebut. "Dia didukung oleh banyak orang untuk waktu yang lama, dan berkat sejarahnya yang panjang, saat ini kekurangannya sudah diketahui."
Pada 2013, Leonardo de Mura , seorang peneliti di Microsoft, meluncurkan proyek Lean. Namanya [lean] mencerminkan keinginan de Moore untuk menciptakan program yang efisien dan bersih. Dia berasumsi bahwa program akan menjadi alat untuk memeriksa keakuratan kode program lain, bukan matematika. Namun, ternyata memeriksa kebenaran sebuah program mirip dengan memeriksa bukti.
“Kami membuat Lean karena tertarik pada pengembangan perangkat lunak, dan ada analogi antara membuat matematika dan menulis kode,” kata de Moore.
Heather Macbeth dari Fordham University, salah satu pengguna Lean
Pada saat Lean dirilis, ada beberapa program pembantu lainnya, termasuk Coq, yang paling mirip dengan Lean. Dasar logis untuk kedua program ini didasarkan pada teori tipe dependen. Namun, Lean menawarkan kesempatan untuk memulai kembali.
Dia dengan cepat menarik ahli matematika. Mereka menggunakannya dengan sangat antusias sehingga mereka mulai menggunakan semua waktu luang de Moore dengan pertanyaan-pertanyaan mereka tentang perkembangan di bidang matematika. "Dia sedikit muak dengan ahli matematika terkemuka dan berkata - mengapa kalian tidak membuat repositori terpisah?" Kata Morrison.
Ahli matematika membuat perpustakaan ini pada tahun 2017. Mereka menyebutnya mathlib dan dengan bersemangat mulai mengisinya dengan pengetahuan matematika dunia, menciptakan sesuatu yang mirip dengan Perpustakaan Alexandria.di abad XXI. Matematikawan membuat dan mengunggah cuplikan matematika digital, secara bertahap membuat katalog untuk Lean. Dan karena mathlib masih baru, mereka dapat belajar dari batasan sistem masa lalu seperti Coq, dan melacak bagaimana materi disusun.
“Ada upaya yang disengaja untuk membuat perpustakaan matematika monolitik, yang semua fragmennya akan bekerja satu sama lain,” kata Macbeth.
Mathlib Alexandrian
The proyek mathlib halaman rumah memiliki grafik yang menunjukkan kemajuan proyek secara real time. Proyek ini memiliki daftar pemimpin yang berinvestasi paling banyak di dalamnya, diurutkan berdasarkan jumlah baris kode [pertama-tama, adalah matematikawan Rusia Yuri Kudryashov / kira-kira. terjemahan.]. Jumlah objek matematika digital juga dihitung: pada awal Oktober, berisi 18.756 definisi dan 39.157 teorema.
Semua bahan matematika ini dapat dicampur untuk membuat matematika dalam Lean. Sejauh ini, jangkauan mereka sangat terbatas, meskipun jumlahnya tampak mengesankan. Hampir tidak ada bidang analisis kompleks atau persamaan diferensial - dan ini adalah dua elemen dasar dari banyak bidang matematika yang lebih tinggi. Selain itu, program ini belum cukup tahu untuk bahkan menggambarkan salah satu Masalah Milenium - masalah matematika yang didefinisikan oleh Clay Mathematical Institute pada tahun 2000 sebagai "masalah klasik penting yang belum terpecahkan selama bertahun-tahun."
mathlib perlahan tapi pasti mengisi. Pekerjaan berlanjut dengan semangat kerja tim. Dalam obrolan Zulip, ahli matematika memilih definisi untuk diformalkan, ditantang untuk menuliskannya, dan memberikan umpan balik yang cepat tentang pekerjaan orang lain.
“Setiap ahli matematika penelitian dapat mempelajari mathlib dan membuat daftar 40 hal yang tidak ada,” kata Macbeth. - Oleh karena itu, dia memutuskan untuk mengisi salah satu kekurangan ini. Dan kesenangan instan dijamin - seseorang akan membaca karya Anda dan memberikan komentar tentangnya dalam waktu 24 jam. "
Banyak add-on ternyata kecil - seperti yang ditemukan Sophie Moreldari Lyon Normal School selama seminar online "Lean for Curious Mathematicians". Penyelenggara konferensi memberikan para peserta pernyataan matematika yang relatif sederhana yang perlu dibuktikan dalam Lean sebagai praktik. Bekerja dengan salah satu dari mereka, Morel menyadari bahwa buktinya membutuhkan lemma - hasil menengah kecil - yang tidak ditemukan di mathlib.
“Itu adalah bagian kecil dari aljabar linier, yang, untuk beberapa alasan, belum ada. Orang-orang yang mengisi mathlib mencoba memahami semuanya, tetapi Anda tidak dapat meramalkan semua opsi, ”kata Morel, yang memasukkan sendiri lemma tiga baris yang diminta ke dalam pangkalan.
Kontribusi lain lebih signifikan. Selama setahun terakhir, Gösel telah bekerja untuk mendefinisikan manifold yang mulus untuk mathlib. Lipatan halus adalah himpunan (seperti garis, lingkaran, atau permukaan bola) yang memainkan peran mendasar dalam studi geometri dan topologi. Mereka juga sering memainkan peran penting dalam masalah dari bidang-bidang seperti teori bilangan dan kalkulus. Kebanyakan penelitian matematika tidak mungkin dilakukan tanpa mereka.
Namun, lipatan halus dapat bersembunyi di balik penyamaran yang berbeda - semuanya tergantung pada konteksnya. Mereka dapat memiliki jumlah dimensi yang terbatas atau tidak terbatas, memiliki batas atau tidak memilikinya, ditentukan melalui berbagai sistem bilangan - pada himpunan nyata, kompleks atau p-adicangka. Mendefinisikan keragaman yang halus seperti mendefinisikan cinta: Anda mengenalinya saat bertemu dengannya, tetapi definisi yang tegas pasti akan menghilangkan beberapa contoh paling jelas dari fenomena ini.
“Saat mendefinisikan hal-hal dasar, Anda tidak perlu membuat pilihan apa pun,” kata Gösel. "Tetapi objek yang lebih kompleks dapat diformalkan dalam 10-20 cara berbeda."
Gösel perlu menjaga keseimbangan antara kekhususan dan generalisasi. “Saya memiliki aturan - saya ingin dapat mendefinisikan 15 penggunaan manifold yang berbeda,” katanya. “Pada saat yang sama, saya tidak ingin definisi tersebut terlalu umum, jika tidak, tidak mungkin untuk bekerja dengannya.”
Definisi yang dia kembangkan cocok dengan 1.600 baris kode - cukup banyak untuk definisi dari mathlib, tapi mungkin tidak terlalu banyak dibandingkan dengan semua kemungkinan matematika yang dia buka untuk Lean.
“Sekarang kita sudah mendapatkan bahasa yang kita butuhkan, kita bisa mulai membuktikan teorema,” katanya.
Menemukan definisi yang benar dari sebuah objek dengan derajat keumuman yang benar adalah pekerjaan utama para ahli matematika yang mengisi mathlib. Pembuat perpustakaan berharap dapat mendefinisikan objek dengan cara yang berguna saat ini, dan pada saat yang sama cukup fleksibel sehingga objek tersebut dapat digunakan dengan cara yang tidak terduga saat ini.
“Kebutuhan akan segala sesuatu yang berguna untuk digunakan di masa depan yang jauh digarisbawahi,” kata Macbeth.
Perfectoids lahir dari latihan
Tetapi Lean bukan hanya alat yang berguna - ini memberikan kesempatan kepada matematikawan untuk menggunakan kembali pekerjaan mereka. Macbeth masih ingat pertama kali dia mencoba program untuk membantu menulis bukti. Saat itu 2019 dan programnya adalah Coq (meskipun sekarang telah beralih ke Lean). Dia tidak bisa berhenti.
“Pada suatu akhir pekan yang gila, saya bekerja dengan program ini selama 12 jam berturut-turut,” katanya. "Itu benar-benar kecanduan."
Ahli matematika lain menggambarkan pengalaman mereka dengan cara yang sama. Lean, kata mereka, seperti permainan komputer - turun ke hormon penghargaan yang sama yang membuat pengontrol game sulit dikesampingkan. "Anda bisa melakukan ini selama 14 jam sehari tanpa merasa lelah dan dalam kondisi terangkat sepanjang hari," kata Livingston. "Anda mendapat tanggapan positif setiap saat."
Sebastien Gösel
Namun komunitas Lean memahami bahwa bagi banyak ahli matematika, tidak ada cukup level dalam program mereka.
"Jika Anda menghitung persentase matematika formal, saya akan mengatakan bahwa kurang dari seperseribu persen sudah siap," kata Christian Szegedi, seorang programmer Google yang mengerjakan sistem AI yang ia impikan untuk dapat membaca dan memformalkan buku teks matematika secara mandiri.
Tapi ahli matematika meningkatkan persentase ini. Jika hari ini mathlib berisi sebagian besar materi yang diajarkan oleh mahasiswa tahun kedua, peserta proyek berharap dapat menambah sisa program dalam beberapa tahun - dan ini akan menjadi pencapaian yang signifikan.
“Dalam 50 tahun sistem ini, tidak ada yang menyarankan: mari kita duduk dan mengatur basis pengetahuan matematika yang konsisten, menjelaskan materi institut,” kata Buzzard. "Kami menciptakan sesuatu yang dapat memahami pertanyaan ujian institut - ini belum pernah terjadi sebelumnya."
Mungkin perlu beberapa dekade sebelum konten mathlib cocok dengan perpustakaan penelitian, tetapi pengguna Lean mendemonstrasikan setidaknya kemungkinan teoretis untuk membuat katalog semacam itu - dan mencapai tujuan ini hanya bergantung pada memasukkan semua matematika dalam database dalam bentuk kode program.
Untuk tujuan ini, tahun lalu Buzzard, Masso dan Johan Kommelin dari Universitas Freiburg di Jerman melaksanakan proyek yang membuktikan kelangsungan mimpi ini. Mereka untuk sementara waktu menunda pengisian pangkalan secara bertahap dengan bahan institut dan pindah ke daerah yang lebih maju. Tujuan mereka adalah untuk mengidentifikasi salah satu inovasi terbesar dalam matematika abad ke-21 - sebuah objek seperti "ruang perfectoid" yang dikembangkan selama sepuluh tahun terakhir oleh Peter Scholze dari Universitas Bonn. Pada 2018, ia menerima Fields Prize untuk karyanya, penghargaan terbesar dalam matematika.
Buzzard, Masso, dan Commelin ingin mendemonstrasikan bahwa, paling tidak secara prinsip, Lean dapat bekerja dengan matematika yang sangat diminati oleh para matematikawan. “Mereka mengambil sesuatu yang sangat kompleks dan baru dan menunjukkan bahwa benda-benda ini dapat dimanipulasi dengan program untuk membantu menulis pembuktian,” kata Mabubi.
Kevin Buzzard
Untuk mendefinisikan ruang perfectoid, tiga ahli matematika perlu menggabungkan lebih dari 3.000 definisi objek matematika dan 30.000 koneksi di antara keduanya. Definisi telah meluas di banyak bidang matematika, dari aljabar hingga topologi dan geometri. Menyatukannya dalam satu definisi adalah demonstrasi yang kuat dari pertumbuhan kompleksitas matematika dari waktu ke waktu - dan mengapa sangat penting untuk mendapatkan dasar untuk mathlib dengan benar.
“Banyak bidang matematika tingkat lanjut mengharuskan Anda mengetahui semua jenis matematika yang diajarkan kepada siswa,” kata Macbeth.
Tritunggal telah berhasil mendefinisikan ruang perfectoid, tetapi sejauh ini hanya ada sedikit ahli matematika yang dapat melakukannya. Banyak lagi definisi matematis yang perlu diperkenalkan ke dalam Lean sebelum program setidaknya dapat merumuskan pertanyaan kompleks di mana ruang perfectoid ini muncul.
"Sangat konyol bahwa Lean tahu apa itu ruang perfectoid, tapi tidak tahu analisis yang rumit," kata Masso.
Buzzard sependapat dengannya, menyebut formalisasi ruang perfectoid sebagai "tipu muslihat" - tipuan yang kadang-kadang ditunjukkan oleh teknologi baru untuk menunjukkan kegunaannya. Dan kali ini triknya berhasil.
“Anda tidak perlu berpikir bahwa berkat pekerjaan kami, semua matematikawan di Bumi mulai menggunakan program untuk membantu menulis bukti,” kata Masso, “tetapi saya pikir banyak dari mereka yang memperhatikan kemungkinan ini dan mulai mengajukan pertanyaan.”
Butuh waktu lama sebelum Lean bisa menjadi bagian nyata dari penelitian matematika. Namun, bukan berarti saat ini acara tersebut merupakan gambaran dari fiksi ilmiah. Para ahli matematika yang terlibat dalam pengembangannya membandingkan pekerjaan mereka dengan meletakkan rel kereta api pertama - awal yang diperlukan dari sebuah perusahaan penting, bahkan jika mereka sendiri mungkin tidak dapat mengendarainya.
"Ini akan menjadi hal yang sangat keren sehingga sebanding dengan masalahnya hari ini," kata Macbeth. "Saya menginvestasikan waktu saya padanya hari ini sehingga seseorang di masa depan dapat memiliki pengalaman yang luar biasa bekerja dengannya."