Status Kemajuan Formalisasi Teorema Terakhir Fermat
(xenaproject.wordpress.com)- Pekerjaan memindahkan pembuktian FLT ke Lean telah berlangsung selama dua bulan, dan definisi R dan T yang diperlukan untuk teorema “R=T” milik Wiles masih belum selesai, tetapi satu hasil aljabar komutatif abstrak sudah berhasil dibuktikan
- Tujuannya bukan menyalin mentah pembuktian asli dari era 1990-an, melainkan membangun pembuktian yang telah digeneralisasi dan disederhanakan berdasarkan karya lanjutan Diamond/Fujiwara, Kisin, Taylor, Scholze, dan lainnya di atas Lean dan mathlib
- Saat memformalkan crystalline cohomology yang dibutuhkan untuk pembuktian modern, muncul masalah bahwa lema kunci dalam makalah Roby tahun 1965, referensi standar untuk struktur divided power, tampak salah
- Brian Conrad menemukan pembuktian alternatif di lampiran buku Berthelot-Ogus, dan Arthur Ogus juga mengatakan ia tahu cara memperbaiki kesalahan di lampiran itu, sehingga proyek dapat berjalan lagi
- Kasus ini menunjukkan risiko bahwa rincian pembuktian matematika modern bergantung pada ingatan pakar dan pengetahuan implisit, serta memperkuat alasan praktis untuk mencatat pembuktian dalam sistem formal
Status terkini pemindahan pembuktian FLT ke Lean
- Pekerjaan mengajarkan pembuktian Teorema Terakhir Fermat (FLT) kepada komputer telah berlangsung selama dua bulan
- Banyak pekerjaan diperlukan untuk mendefinisikan apa itu R dan T dalam teorema “R=T”, inti dari pembuktian Wiles, di Lean, dan kedua definisi itu masih belum selesai
- Mahasiswa PhD Andrew Yang telah membuktikan hasil aljabar komutatif abstrak yang diperlukan
- Hasilnya berbentuk “jika ring abstrak R dan T memenuhi berbagai syarat teknis, maka keduanya sama”
- Draf saat ini dipublikasikan sebagai blueprint
- Sistem yang digunakan adalah Lean dan pustaka matematika mathlib
- Siapa pun yang sedikit memahami Lean dan teori bilangan dapat berpartisipasi melalui contribution guidelines, project dashboard, dan issue
Mengapa pembuktian era 1990-an tidak dipindahkan apa adanya
- Proyek ini tidak memformalkan pembuktian Wiles dari era 1990-an secara apa adanya
- Setelah itu, pembuktiannya telah dibuat lebih umum dan lebih sederhana lewat karya Diamond/Fujiwara, Kisin, Taylor, Scholze, dan lainnya
- Tujuannya bukan hanya membuktikan FLT, tetapi juga membangun hasil yang lebih umum dan lebih kuat di dalam Lean
- Jika revolusi matematika AI benar-benar terjadi dan Lean menjadi komponen penting, maka akan berguna bila komputer memiliki definisi-definisi inti teori bilangan modern dalam bentuk yang dapat dipahami
Divided powers yang dibutuhkan untuk crystalline cohomology
- Pembuktian yang hendak diformalkan menggunakan crystalline cohomology, yang tidak ada dalam pembuktian asli Wiles
- Teori ini berkembang di Paris pada 1960-an hingga 1970-an, dan Berthelot meletakkan fondasinya berdasarkan gagasan Grothendieck
- Fungsi eksponensial dan logaritma klasik penting untuk memahami geometri diferensial dan de Rham cohomology, tetapi tidak bekerja begitu saja dalam situasi aritmetika seperti characteristic p
- Divided power structures, yang dikembangkan dalam makalah-makalah Roby pada 1960-an, berperan penting untuk membangun fungsi-fungsi serupa yang dapat dipakai dalam situasi aritmetika
- Untuk mengajarkan crystalline cohomology kepada Lean, divided powers harus diformalkan terlebih dahulu
Masalah pada literatur Roby yang terungkap saat bekerja di Lean
- Antoine Chambert-Loir dan Maria Ines de Frutos Fernandez sedang memformalkan teori divided powers di Lean
- Selama musim panas, Lean mengungkap masalah dalam argumen manusia di literatur standar, dan setelah diperiksa, lema kunci dalam karya Roby tampak salah
- Secara teknis, makalah Berthelot tidak mengembangkan teori divided powers dari awal, melainkan menggunakan karya Roby “Les algebres a puissances divisees”
- Makalah itu terbit di Bull Sci Math, 2ième série, 89, 1965, hlm. 75-91
- Lemme 8 di hlm. 86 tampak salah, dan tidak jelas bagaimana membetulkan pembuktiannya
- Pembuktian itu salah mengutip lema lain dari makalah Roby tahun 1963 di Ann Sci ENS
- Pernyataan yang benar adalah
Gamma_A(M) tensor_A R = Gamma_R(M tensor_A R), tetapi dalam penerapannya satu tensor product terlewat
- Masalah ini merusak pembuktian Roby bahwa divided power algebra dari sebuah module memiliki divided powers, dan akibatnya menghalangi definisi ring
A_cris
Situasinya lebih dekat ke “pembuktiannya kosong” daripada “teorinya salah”
- Ini tidak berarti crystalline cohomology sendiri pada dasarnya salah
- Teorema-teorema utamanya masih tampak benar, tetapi pembuktian yang diikuti Antoine dan Maria Ines tidak lengkap
- Karena Roby, Grothendieck, dan Berthelot semuanya telah wafat, para pakar asli tidak bisa lagi ditanya langsung
- Sejumlah pakar menilai bahwa meski lema perantara itu salah, pembuktian hasil utama tetap bisa diperbaiki
- Dalam formalisasi, keyakinan bahwa “ini seharusnya bisa diperbaiki” tidak cukup; yang dibutuhkan adalah pembuktian yang benar-benar telah diperbaiki
Lampiran Berthelot-Ogus membuka jalur memutar
- Tadashi Tokieda menceritakan kisah ini kepada Brian Conrad di Stanford, dan Conrad bertanya apa yang dimaksud dengan kabar bahwa crystalline cohomology salah
- Setelah mendengar rincian teknisnya, Conrad setuju bahwa memang tampak ada masalah lalu mulai meninjaunya
- Beberapa jam kemudian, Conrad memberi tahu bahwa di lampiran buku crystalline cohomology karya Berthelot-Ogus ada pembuktian lain bahwa universal divided power algebra of a module memiliki divided powers
- Dari sudut pandang Conrad, pendekatan itu tampak baik-baik saja, sehingga pembuktian bisa dilanjutkan kembali
- Setelah itu, saat makan siang dengan Arthur Ogus di Berkeley dan menyampaikan bahwa lampiran tersebut menyelesaikan masalah, Ogus menjawab bahwa ada beberapa kesalahan juga di lampiran itu, tetapi ia tahu cara memperbaikinya
Mengapa literatur matematika modern membutuhkan formalisasi
- Proses ini menunjukkan bahwa cara manusia mendokumentasikan matematika modern mungkin belum cukup kokoh
- Banyak fakta tetap berada pada level “para pakar tahu ini”, dan bisa jadi tidak pernah dirapikan secara tepat dalam literatur
- Gagasan pentingnya mungkin cukup kokoh untuk bertahan dari guncangan seperti ini, tetapi rincian pembuktian yang sesungguhnya bisa jadi tidak berada di tempat yang diharapkan
- Mencatat matematika dengan benar dalam sistem formal dapat sangat mengurangi kemungkinan kesalahan
- Bahkan bagi matematikawan yang bukan formalis, jika mesin ingin mempelajari argumen manusia dan kelak melakukan matematika sendiri, maka proses mengajarkan argumen itu ke mesin harus dilakukan terlebih dahulu
- Maria Ines mempresentasikan formalisasi divided powers di seminar Cambridge Formalization of Mathematics dalam presentasi, dan masalah-masalah tersebut dipahami telah dibereskan
- Proyek ini telah kembali ke jalurnya, tetapi tetap ada kemungkinan literatur kembali menghambat kemajuan
1 komentar
Opini Hacker News
Saya teringat saat di sekolah pascasarjana menulis kode cepat untuk membantu pendekatan komputasional dosen pembimbing saya terhadap konjektur Birch–Swinnerton-Dyer
Di sebuah seminar teori bilangan di kota terdekat, saya ditanya apakah “tujuannya memperkuat bukti yang mendukung konjektur itu”, dan ketika saya tersenyum lalu menjawab, “Tidak, saya justru ingin menemukan contoh tandingan,” para pakar sangat marah
Teori bilangan begitu tua dan dalam sehingga menulis disertasi doktoral di bidang itu terasa nyaris seperti langkah pertama menjadi pemula; meski saya tahu notasi dan definisinya, saya belum menjangkau intuisi di bawahnya
Jadi kemarahan para pakar terhadap ucapan “saya berharap ada contoh tandingan” meninggalkan rasa ingin tahu, bukan rasa takut; saya penasaran apa yang mereka lihat tetapi belum bisa mereka ungkapkan dengan kata-kata
Kemajuan formalisasi seperti ini membuat matematika jauh lebih mudah diakses bagi orang yang lebih akrab dengan pemrograman
Kekhawatiran bahwa formalitasnya kurang itu sah, tetapi menurut saya respons yang tepat terhadap kekhawatiran bukanlah menghindar, melainkan rasa ingin tahu
Kalau pemula hijau seperti Anda menemukan contoh tandingan lewat perhitungan kasar dan menjadi terkenal dalam semalam, seluruh usaha dan bangunan itu bisa runtuh, jadi saya bisa membayangkan mereka marah
Jika saya memberi nasihat sekolah pascasarjana matematika kepada diri saya yang masih muda dulu, saya akan berkata agar untuk setiap tugas “buktikan X” yang tidak sepele, setidaknya 1/4 waktu dipakai untuk mencari contoh tandingan
Dalam tugas kuliah, 99% upaya itu akan gagal, tetapi wawasan Anda tentang masalahnya akan jauh lebih besar, dan pada 1% sisanya Anda bisa tampak seperti jenius
Begitu masuk ke riset matematika sungguhan, peluang itu berubah jauh lebih menguntungkan bagi pendekatan yang mengutamakan contoh tandingan
Saat masih mahasiswa, saya ingat seorang teman bercerita bahwa seseorang baru saja menyelesaikan hari pertama seminarnya, dan semua orang heboh karena yakin ia akan membuktikan Teorema Terakhir Fermat
Orang itu adalah Andrew Wiles, dan setelah itu ia menghabiskan beberapa bulan untuk memperbaiki masalah yang ditemukan sebelum publikasi, hingga akhirnya seluruhnya diterbitkan
Bagi saya yang belajar matematika, itu peristiwa yang luar biasa mendebarkan, jadi ketika melihat ungkapan “bukti kuno dari 1990-an”, saya benar-benar merasa tua
Hampir seluruh kelas adalah mahasiswa pascasarjana matematika, dan rasanya saya bahkan tidak memahami 20% materinya
Saya suka bagian ketika Lean melakukan hal menjengkelkan yang kadang dilakukannya: ia mengeluhkan penyajian argumen ala manusia dalam literatur standar, dan setelah diperiksa lebih teliti, ternyata memang ada bagian yang kurang dalam argumen manusia itu
Terlepas dari kejengkelan yang bercampur humor, ini hal yang luar biasa, dan Lean serta pembukti teorema lain tampaknya akan menjadi alat penting dalam matematika ke depan
Bagian tentang buruknya dokumentasi matematika modern terasa mirip dengan UI/UX/desain web
Desainer membuat mockup, prototipe, dan alur interaksi yang informal serta tidak presisi, lalu menyerahkannya kepada developer; developer harus memformalkannya menjadi kode dan menjelaskannya secara tepat kepada mesin
Dalam proses itu, mereka pasti menemukan lubang seperti skenario interaksi atau jalur kode yang tidak dipertimbangkan desain, dan kadang cacat desain besar terungkap sehingga developer atau desainer harus menutupinya
Desain dan pengembangan adalah peran yang berbeda dan menuntut cara berpikir berbeda; sebagian besar desainer menunjukkan resistensi kuat terhadap bekerja dan berpikir seperti developer
Setelah kegagalan itu, kita belajar bahwa matematika tidak bisa diformalkan sepenuhnya, dan ini menunjukkan masalah mendasar dalam pendekatan yang ingin melakukan matematika dengan AI
Jika tertarik dengan topik ini, ada baiknya melihat kode aslinya
Contoh: https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/M...
Cetak biru yang menjelaskan struktur keseluruhan kodenya juga layak dilihat: https://imperialcollegelondon.github.io/FLT/blueprint/
Dari sudut pandang orang luar, sangat menarik melihat seperti apa kode Lean dan bagaimana orang-orang berkontribusi
Saya juga suka bahwa tidak perlu unit test. Dalam arti tertentu, proposisi bukti akhir adalah unit test-nya
Misalnya, contoh-contoh sederhana dan contoh tandingan untuk memastikan suatu definisi tidak kosong berperan seperti itu
Dari sudut pandang saya yang pernah menekuni matematika murni, masalah besarnya adalah para matematikawan hampir tidak pernah menyajikan bukti yang sepenuhnya mandiri
Tidak ada insentif untuk melakukannya, dan kadang para penulis bahkan bangga dengan “detail dihilangkan”
Pada akhirnya, jika menginginkan bukti ketat yang memungkinkan setiap langkah logika diikuti, seorang pakar harus mengisi celah-celah yang tidak mudah ditemukan dalam literatur
Itu kadang baru mungkin jika orang seperti itu menulis buku yang menjelaskan semuanya, dan terkadang itu pun belum cukup
Jika hanya melihat apa yang tercatat, banyak bagian matematika modern berdiri di atas fondasi yang rapuh
Makalah riset matematika ditulis untuk pakar lain di bidang yang sama, dan kadang detailnya memang terlalu sedikit sehingga sering dikeluhkan saat peer review
Namun jika semua detail benar-benar disediakan, makalah akan menjadi jauh lebih panjang
Contoh yang bisa diselesaikan dengan latar belakang matematika SMA yang kuat adalah soal membuktikan bahwa ada konstanta C, X > 0 sehingga untuk suatu bilangan riil x > X,
log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4x + 3)) < CxPernyataan semacam ini selalu muncul dalam teori bilangan analitik, dan bagi pakar itu jelas, sehingga dalam makalah hampir selalu ditulis tanpa bukti
Jika dibuat bukti yang lengkap dan ketat, hasilnya panjang dan membosankan, dan tidak ada pakar yang ingin membacanya
Sikap seperti ini memang punya biaya kompromi, tetapi tampaknya masih pada tingkat yang bisa dikelola
Ini terdengar seperti tahap ketiga yang disebut Tao, yaitu intuisi yang terinformasi
Ia berkata, “Kalau Anda sudah melakukan sesuatu 100 kali, Anda boleh mengatakan ‘seperti yang mudah diamati’ lalu lanjut”
Dengan kata lain, saya memahaminya sebagai pekerjaan seseorang yang memiliki basis data di kepalanya untuk mencari apakah prasyarat suatu teorema dan kesimpulan kalimat berikutnya cocok
Atau saya penasaran apakah ada matematika yang saat ini tidak bisa diekspresikan dengan cara yang dapat dievaluasi proof checker
Atau mungkin penggunaan proof checker belum seluas yang saya kira. Kedengarannya mirip dengan posisi bahasa bertipe statis dalam pemrograman
Maksudnya, apakah pernah ada kasus ketika bukti yang diterima luas ternyata memiliki cacat fatal karena bagian yang dilewati dengan lambaian tangan
Jika tidak pernah terjadi, saya bisa memahami mengapa ada sikap longgar dalam menuliskan detail
Saya selalu bertanya-tanya apakah intuisi bahwa “crystalline cohomology sudah begitu banyak digunakan sejak 1970-an, jadi kalau ada masalah pasti sudah terungkap sejak lama” benar-benar tepat
Apakah benar-benar semustahil itu jika seluruh cabang matematika dikembangkan di atas bukti yang cacat, lalu cabang itu ternyata begitu saja salah
Ia melihat sendiri sebuah bidang runtuh karena kesalahan pada “lemma pertama di halaman pertama” makalah fondasionalnya
Rangkaian dari pekerjaan awal tentang UniMath, tahun khusus di IAS, hingga buku HoTT bisa dibilang telah mengangkat topik formalisasi matematika ke posisinya saat ini
Jika fondasinya salah, salah satu contoh tandingan itu bisa saja juga membantah teorema dasar, sehingga membangun di atas fondasi yang keliru justru besar kemungkinan menyingkap cacat pada fondasi tersebut
Serupa dengan itu, ketika matematika kadang diterapkan untuk membuat prediksi, jika matematikanya salah maka prediksinya juga salah, dan prediksi yang salah itu akan menarik banyak perhatian
Sebenarnya kata “bidang” agak menyesatkan; banyak teori lebih mirip simpul yang terikat dengan berbagai teori lain di seluruh matematika
Teori-teori itu pun kembali terhubung dengan teori lain
Akan sangat aneh jika hanya fondasinya yang runtuh secara logis tanpa berdampak pada bagian lain dari simpul ini
Segumpal besar matematika mengambang yang secara internal sepenuhnya konsisten tetapi hanya memiliki satu kesalahan, dalam kasus kohomologi di tulisan ini, sulit saya bayangkan
Secara ketat, ini lebih dekat ke sikap filosofis, tetapi saya ingin percaya bahwa banyak bagian matematika saat ini dalam suatu makna ditemukan secara alami
Spoiler-nya: dunia tetap berjalan
Selama kira-kira setahun terakhir, saya sesekali mencoba memformalkan sebagian mata kuliah analisis kompleks tingkat sarjana di Lean
Banyak hal yang bisa dipelajari dan terasa memuaskan, tetapi kadang juga membuat frustrasi
Baru belakangan ini saya bisa mendefinisikan sepenuhnya bentuk polar sebagai bijeksi dari C* ke (-pi,pi] x R, karena saya bersikeras mendefinisikannya “dari awal” meskipun bilangan kompleks, deret pangkat, exp, dan sin sudah ada di mathlib
Kemungkinan besar sebagian besar kesulitannya muncul karena saya hanya punya gelar sarjana matematika, belum terbiasa dengan Lean/mathlib, dan tidak ada orang yang membimbing. Namun komunitas Zulip sangat membantu
Banyak hasil di mathlib dinyatakan dengan cukup abstrak, sehingga sulit memahami bagaimana hasil-hasil itu terhubung dengan teorema standar tingkat sarjana, atau apakah teorema semacam itu ada di mathlib
Ini masuk akal bagi komunitas matematika riset, tetapi bagi saya pribadi menjadi hambatan besar, dan jika Lean lebih banyak dipakai dalam pendidikan, hal serupa bisa menjadi masalah. Meski begitu, ini hal yang bisa dibereskan seiring waktu
Menurut saya otomatisasi pembuktian masih belum memadai
Terlalu banyak hal yang lebih sulit dibuktikan daripada semestinya, dan khususnya konversi tipe adalah yang paling membuat saya tidak puas
Dalam matematika biasa, bilangan real adalah subset dari bilangan kompleks, sehingga apa pun yang benar untuk semua bilangan kompleks otomatis benar untuk semua bilangan real. Namun di Lean, keduanya adalah tipe berbeda dan harus bolak-balik lewat pemetaan injektif/operasi konversi tipe, sehingga inti pembuktian menjadi kabur
Ini menjadi sangat berantakan terutama saat konversi tipe menumpuk, misalnya dari bilangan natural ke bilangan real, lalu ke bilangan kompleks
Tentu saja ini mungkin masalah khas topik ini, dan di bidang seperti aljabar yang menangani pemetaan eksplisit, rasanya akan jauh lebih alami
Sangat mudah mendapatkan arahan tentang cara memakai mathlib, apa saja yang tersedia, dan di mana letaknya
Masalah konversi tipe yang bertumpuk biasanya diselesaikan dengan taktik
norm_castBahkan jika bukan pertanyaan spesifik, bila Anda menyebutkannya sepintas atau orang melihat gaya pembuktian yang terlalu rumit dalam kode, Anda bisa mendapat saran tentang taktik yang sebelumnya tidak Anda ketahui
Jika Anda hanya merasa formalisasi terlalu sulit dan tidak tahu teknik apa yang harus dipakai, Anda bisa mengambil satu pembuktian tidak memuaskan yang sudah susah payah dibuat, menjadikannya contoh terisolasi, lalu bertanya agar orang-orang mencoba memendekkannya
Pertanyaan seperti ini biasanya disambut baik dan semua orang banyak belajar
Utas ini tampaknya berkaitan dengan cara menulis matematika dengan baik
Saya telah membaca, menulis, mengajar, menerapkan, dan menerbitkan matematika selama beberapa dekade, serta meraih doktor di bidang matematika terapan
Memang benar ada masalah dalam penulisan matematika, dan sebagian matematika ditulis dengan sangat buruk
Namun ada juga matematika yang ditulis cukup baik
Setidaknya semua simbol harus didefinisikan sebelum digunakan, memberi motivasi sebelum menyajikan matematika itu membantu, dan kadang penjelasan intuitif juga berguna
Membaca matematika yang ditulis dengan baik secara cermat membantu mempelajari penulisan matematika
Contohnya adalah Finite-Dimensional Vector Spaces karya Paul R. Halmos, Advanced Calculus karya R. Creighton Buck, Mathematical Analysis karya Tom M. Apostol, Real Analysis karya H. L. Royden, Real and Complex Analysis karya Walter Rudin, Probability karya Leo Breiman, dan Mathematical Foundations of the Calculus of Probability karya Jacques Neveu
Penulis mencoba memverifikasi Teorema Terakhir Fermat persis seperti cara ia dikembangkan dalam literatur, dan dalam prosesnya menemukan bahwa lemma bantu yang menopang satu subbidang tidak benar dalam bentuk saat lemma itu digunakan
Meski begitu, alasan ia percaya bidang tersebut pada umumnya masih bisa diselamatkan adalah keyakinan bahwa jika benar-benar salah, seseorang pasti sudah menemukan hasil negatif
Kini ia harus menemukan pengganti yang tepat untuk menopang bidang tersebut
Penulisnya cukup menyenangkan dalam menulis, sehingga meski saya tidak memahami kira-kira separuhnya, pengalaman membacanya terasa aneh karena tetap mudah dibaca
Saya menemukan vitiated sebagai kata yang bagus untuk dipakai ketika sebuah pembuktian terbantahkan atau ditemukan cacat
Saya menyukainya karena tidak terlalu menimbulkan kesalahpahaman bahwa kesimpulannya telah terbukti salah, tetapi tetap menyampaikan bahwa pembuktian itu telah rusak dan membutuhkan pembuktian baru atau perbaikan