terence tao menawarkan hadiah untuk otak paling kuat di internet! manusia ai menumbangkan masalah matematika? netizen versailles sudah tiada
2024-09-29
한어Русский языкEnglishFrançaisIndonesianSanskrit日本語DeutschPortuguêsΕλληνικάespañolItalianoSuomalainenLatina
laporan kebijaksanaan baru
editor: aeneas mengantuk sekali[pengantar kebijaksanaan baru]baru-baru ini, tao zhexuan meluncurkan tantangan kepada sebagian besar netizen dan penggemar matematika: bisakah para penggemar matematika populer, asisten pembuktian, asisten otomatis, dan ai bergabung untuk membuktikan masalah matematika yang meluas hingga beberapa kali lipat?
ingin berpartisipasi dalam proyek penelitian matematika "crowdsourcing" yang diluncurkan oleh terence tao?penelitian matematika pembuktian yang dibantu ai menjadi semakin mungkin dilakukan
masing-masing dari mereka cukup akrab dengan aspek-aspek proyek untuk memvalidasi kontribusi masing-masing.namun jika anda ingin mengorganisir proyek penelitian matematika berskala besar, terutama proyek yang melibatkan kontribusi publik, itu jauh lebih merepotkan.alasannya adalah sulitnya memverifikasi kontribusi setiap orang.pada akhir tahun 2023, terence tao mengumumkan bahwa proyek lean4, yang meresmikan bukti dugaan polinomial freiman-ruzsa, berhasil setelah tiga minggu (gambar menunjukkan status terbaru)sadarilah bahwa satu kesalahan dalam satu bagian argumen matematika dapat menyebabkan keseluruhan proyek gagal.selain itu, mengingat kompleksitas proyek matematika pada umumnya, tidak realistis mengharapkan anggota masyarakat dengan pendidikan sarjana matematika untuk memberikan kontribusi yang berarti.dari sini kita juga dapat mengetahui bahwa menggabungkan alat ai ke dalam proyek penelitian matematika juga merupakan hal yang sangat menantang.karena ai dapat menghasilkan argumen yang tampak masuk akal namun sebenarnya tidak masuk akal, diperlukan verifikasi tambahan sebelum bagian yang dihasilkan ai dapat ditambahkan ke proyek.untungnya, bahasa yang didukung bukti seperti lean menawarkan cara potensial untuk mengatasi hambatan ini dan memungkinkan kolaborasi antara ahli matematika profesional, masyarakat luas, dan alat ai.pendekatan ini didasarkan pada premis bahwa proyek dapat dipecah secara modular menjadi bagian-bagian kecil yang dapat diselesaikan tanpa harus memahami keseluruhan proyek.contoh-contoh saat ini terutama mencakup proyek-proyek yang memformalkan hasil matematika yang ada (seperti formalisasi dugaan pfr yang baru-baru ini dibuktikan oleh marton).formalisasi ini terutama dilakukan melalui crowdsourcing oleh kontributor manusia (termasuk ahli matematika profesional dan masyarakat yang berkepentingan).pada saat yang sama, ada juga beberapa upaya yang muncul untuk memperkenalkan lebih banyak alat otomatis untuk menyelesaikan tugas, termasuk pembukti teorema otomatis tradisional dan alat berbasis ai yang lebih modern.menjadi mungkin untuk mengeksplorasi masalah matematika baru
dan,terence taoparadigma baru ini juga diyakini dapat digunakan tidak hanya untuk memformalkan matematika yang sudah ada, tetapi juga untuk mengeksplorasi matematika yang benar-benar baru!di masa lalu, dia dan penggantinya mengorganisir proyek kolaborasi online "polymath", yang merupakan contoh yang baik.namun, proyek ini tidak memasukkan bahasa pendukung bukti ke dalam alur kerjanya, dan kontribusi harus dikelola dan diverifikasi oleh moderator manusia, yang sangat memakan waktu dan membatasi perluasan lebih lanjut dari proyek-proyek ini.sekarang, tao zhexuan berharap menambahkan bahasa tambahan bukti dapat memecahkan hambatan ini.dia khususnya tertarik pada apakah mungkin untuk menggunakan alat-alat modern untuk mengeksplorasi suatu kelas masalah matematika secara bersamaan, daripada berfokus hanya pada satu atau dua masalah pada satu waktu.intinya, pendekatan ini bersifat modular untuk tugas-tugas yang berulang, dan crowdsourcing serta alat otomatisasi bisa sangat berguna jika ada platform yang siap mengoordinasikan semua kontribusi secara ketat.masalah matematika jenis ini tidak akan dapat diukur dengan menggunakan metode sebelumnya. kecuali jika anda perlahan-lahan menjelajahi satu titik data pada satu waktu dengan masing-masing makalah selama bertahun-tahun hingga anda mendapatkan intuisi yang masuk akal tentang masalah semacam ini.selain itu, memiliki kumpulan data masalah yang besar dapat membantu melakukan evaluasi kinerja berbagai alat otomatisasi dan membandingkan efisiensi alur kerja yang berbeda.pada bulan juli tahun ini, jumlah busy beaver kelima dipastikan menjadi 47.176.870.beberapa proyek komputasi crowdsourcing sebelumnya, seperti great internet mersenne prime search (gimps), memiliki semangat yang serupa dengan proyek ini, meskipun mereka menggunakan mekanisme bukti kerja yang lebih tradisional, daripada membuktikan bahasa tambahan.terence tao mengatakan dia tertarik untuk mengetahui apakah ada contoh lain dari proyek crowdsourcing yang mengeksplorasi ruang matematika, dan apakah ada pembelajaran yang dapat digunakan.tao zhexuan mengusulkan proyek baru
untuk tujuan ini, tao sendiri mengusulkan sebuah proyek untuk menguji lebih lanjut paradigma ini.proyek ini terinspirasi oleh pertanyaan mathoverflow tahun lalu.segera setelah itu, tao zhexuan membahasnya lebih lanjut di mathstodon miliknya.masalah ini termasuk dalam bidang aljabar universal dan melibatkan eksplorasi teori persamaan sederhana golongan asal (magma) skala menengah.grup asal adalah grup yang dilengkapi dengan operasi binerhimpunan g.awalnya, operasi o ini tidak memiliki aksioma tambahan apa pun, sehingga grup asli itu sendiri adalah struktur yang relatif sederhana.tentu saja, dengan menambahkan aksioma tambahan, seperti aksioma identitas atau aksioma asosiatif, kita dapat memperoleh objek matematika yang lebih familiar seperti grup, semigrup, atau monoid.di sini kita tertarik pada aksioma kesetaraan (bebas konstan). aksioma ini berkaitan dengan persamaan ekspresi yang dibangun dari operasi o dan satu atau lebih variabel yang tidak diketahui di g.dua contoh umum dari aksioma tersebut adalah hukum komutatif xoy = yox dan hukum asosiatif (xoy) oz = xo (yoz).dimana x, y, z adalah variabel yang tidak diketahui pada golongan asal g.di sisi lain, aksioma identitas (kiri) eox = x tidak dianggap sebagai aksioma persamaan di sini karena melibatkan konstanta e ∈ g. aksioma yang melibatkan konstanta tidak dibahas dalam penelitian ini.selanjutnya, untuk menggambarkan proyek penelitian yang digagasnya, terence tao memperkenalkan sebelas contoh aksioma kesetaraan tentang kelompok primitif.aksioma kesetaraan ini adalah persamaan yang hanya melibatkan operasi grup primitif dan variabel yang tidak diketahui—jadi, misalnya persamaan 7 mewakili aksioma komutatif, sedangkan persamaan 10 mewakili aksioma asosiatif.aksioma konstan persamaan 1 adalah yang terkuat, karena membatasi grup asli g untuk memiliki paling banyak satu elemen; sebaliknya, aksioma refleksif persamaan 11 adalah yang terlemah, dan semua grup asli memenuhi aksioma ini.selanjutnya, kita dapat menelusuri hubungan derivasi antara aksioma-aksioma ini: aksioma manakah yang dapat menyimpulkan aksioma mana?misalnya, persamaan 1 mengarah ke semua aksioma lain dalam daftar ini, yang selanjutnya mengarah ke persamaan 11.persamaan 8 dapat digunakan sebagai kasus khusus untuk menurunkan persamaan 9, yang selanjutnya dapat digunakan sebagai kasus khusus untuk menurunkan persamaan 10.hubungan derivasi selengkapnya antara aksioma-aksioma tersebut dapat dijelaskan dengan diagram hasse berikut:hasil ini secara khusus menjawab pertanyaan di situs q&a matematika mathoverflow: apakah terdapat aksioma persamaan antara aksioma konstanta (persamaan 1) dan aksioma asosiatif (persamaan 10).perlu dicatat bahwa sebagian besar hubungan implikasi di sini mudah dibuktikan. namun, terdapat hubungan implikasi yang tidak sepele.hubungan ini ditemukan dalam jawaban postingan mathoverflow yang terkait erat dengan pertanyaan sebelumnya:proposisi 1: persamaan 4 menyiratkan persamaan 7bukti: misalkan g memenuhi persamaan 4ini berlaku untuk semua x,y ∈ g.khususnya, jika y = xox, maka (xox) o (xox) = (xox) ox.menerapkan (1) lagi, kita dapat menyimpulkan bahwa xox adalah idempoten:sekarang, ganti x dengan xox pada (1) dan gunakan (2), kita peroleh (xox) oy = yo (xox).secara khusus, xox dan yoy dapat dipertukarkan:selanjutnya dengan menerapkan (1) dua kali, diperoleh (xox) o (yoy) = (yoy) ox = xoy.oleh karena itu, (3) dapat disederhanakan menjadi xoy = yox, yaitu persamaan 7.formalisasi proses argumentasi di atas dapat ditemukan dalam lean.namun perlu dicatat bahwa pertanyaan umum mengenai penentuan apakah suatu rangkaian aksioma kesetaraan menentukan rangkaian aksioma kesetaraan yang lain masih belum dapat diputuskan.oleh karena itu, situasi di sini agak mirip dengan tantangan "busy beaver", yaitu, setelah melewati titik kompleksitas tertentu, kita pasti akan menghadapi masalah yang belum terselesaikan, namun sebelum mencapai ambang batas ini, kita masih berharap dapat menemukan masalah dan fenomena yang menarik;diagram hass di atas tidak hanya menegaskan hubungan keterikatan antara aksioma-aksioma kesetaraan yang terdaftar, tetapi juga menegaskan hubungan non-implikasi antara aksioma-aksioma tersebut.misalnya, seperti terlihat pada gambar, aksioma komutatif persamaan 7 tidak menyiratkan aksioma persamaan 4 (x + x) + y = y + x.untuk membuktikannya, cari saja contoh grup primitif yang memenuhi aksioma komutatif persamaan 7 tetapi tidak memenuhi aksioma persamaan 4.misalnya, dalam kasus ini, kita dapat memilih himpunan bilangan asli n, yang operasinya adalah xoy := x+y.secara lebih umum, diagram tersebut menegaskan hubungan non-implikasi berikut, yang (bersama dengan hubungan implikasi yang telah disebutkan) secara lengkap menggambarkan rangkaian hubungan implikasi yang diurutkan sebagian di antara sebelas aksioma ini:di sini, tao zhexuan mengajak pembaca untuk mengajukan contoh tandingan untuk melengkapi beberapa pembuktian.contoh tandingan yang paling sulit ditemukan adalah persamaan 9 tidak dapat menyimpulkan persamaan 8.solusi dapat diberikan dengan menggunakan lean.selain itu, tao zhexuan juga menyediakan repositori github yang berisi bukti lean dari semua hubungan inklusi dan anti-inklusi di atas.terlihat bahwa menghitung diagram haas dari 11 persamaan saja sudah agak rumit.proyek yang diusulkan oleh terence tao adalah upaya untuk memperluas diagram hass ini beberapa kali lipat untuk mencakup kumpulan persamaan yang lebih luas.himpunan yang ia usulkan adalah ε, himpunan persamaan menggunakan operasi grup asli o paling banyak empat kali, hingga aksioma refleksivitas dan simetri persamaan penjumlahan diberi label ulang.ini mencakup sebelas persamaan yang disebutkan di atas, namun masih banyak lagi.ingatlah bahwa bilangan catalan c_n adalah banyaknya cara untuk membentuk ekspresi menggunakan operasi biner o (diterapkan pada n+1 variabel placeholder); dan jika diberi rangkaian m variabel placeholder, bilangan lonceng b_m adalah jumlah cara variabel-variabel ini nama yang ditetapkan (yang dapat diberi label ulang), yang memungkinkan placeholder tertentu diberi nama yang sama.oleh karena itu, dengan mengabaikan simetri, banyaknya persamaan yang melibatkan paling banyak empat operasi adalahbanyaknya persamaan yang ruas kiri dan ruas kanannya sama adalahini setara dengan aksioma refleksif (persamaan 11).sisa 9118 persamaan muncul berpasangan karena persamaannya simetris, sehingga ukuran total ε adalah
tao zhexuan mengatakan bahwa dia belum membuat daftar lengkap identitas tersebut, namun dia menduga hal itu dapat dengan mudah dilakukan menggunakan python.dengan menggunakan alat ai, anda seharusnya dapat menghasilkan sebagian besar kode yang diperlukan.dia mengatakan dia tidak tahu seperti apa bentuk geometri ε.akankah sebagian besar persamaan tidak dapat dibandingkan satu sama lain? apakah akan dibagi menjadi aksioma “kuat” dan aksioma “lemah”?kini, area pesan terence tao mendapat puluhan komentar.pembaca yang tertarik, tao zhexuan juga telah menyampaikan undangan kepada anda.
