Relay yang menjangkau lebih daripada 300 tahun: Diilhamkan oleh Terence Teru, ahli matematik memutuskan untuk menggunakan AI untuk memformalkan bukti Teorem Terakhir Fermat.

Diinspirasikan oleh Terence Tao, semakin ramai ahli matematik mula mencuba menggunakan kecerdasan buatan untuk penerokaan matematik. Kali ini, sasaran mereka ialah Teorem Terakhir Fermat, salah satu daripada sepuluh masalah matematik paling sukar di dunia. Teorem Terakhir Fermat ialah masalah matematik yang sangat kompleks yang belum ada penyelesaian yang boleh dilaksanakan setakat ini. Ahli matematik berharap dengan kuasa pengkomputeran yang berkuasa dan algoritma pintar kecerdasan buatan, mereka boleh meneroka dalam matematik

Teorem Terakhir Fermat, juga dikenali sebagai "Teorem Terakhir Fermat (FLT)", dicipta pada abad ke-17 yang Dicadangkan oleh Perancis. ahli matematik Pierre de Fermat. Ada kisah lagenda disebaliknya. Dikatakan bahawa sekitar tahun 1637, ketika Fermat sedang membaca terjemahan Latin Aritmetik Diophantus, dia menulis di sebelah Proposisi 8 Jilid 11: "Bahagikan nombor padu kepada hasil tambah dua nombor padu, atau Tidak mustahil untuk membahagikan yang keempat. kuasa ke dalam jumlah dua kuasa keempat, atau secara amnya untuk membahagikan kuasa yang lebih tinggi daripada yang kedua kepada jumlah dua kuasa yang sama kuasa "Saya yakin bahawa saya telah menemui sesuatu tentang ini. Ini adalah demonstrasi yang indah, tetapi malangnya ruang kosong di sini terlalu kecil untuk menulisnya. ”

Apa yang dinyatakan dalam perenggan ini ialah kandungan teorem terakhir Fermat: apabila integer n>2, persamaan tentang x^n + y^n=z^n tidak mempunyai penyelesaian integer positif

Fei Ma berkata bahawa dia tahu bagaimana untuk membuktikannya, tetapi dia tidak menulisnya kerana ruang kosong dalam buku itu terlalu kecil kemudiannya timbul kontroversi tentang kesahihan cerita itu dan sama ada Fermat benar-benar mengetahui kaedah pembuktian lebih daripada 300 tahun, ahli matematik telah bekerja keras untuk membuktikan teorem terakhir Fermat Hanya pada tahun 1995, Profesor Andrew Wiles dari Universiti Princeton di Amerika Syarikat akhirnya menyelesaikan buktinya dalam 130 halaman

Sekarang teorem terakhir Fermat telah terbukti, apa lagi yang boleh dilakukan oleh ahli matematik dengan AI? dan teori set) untuk menyatakan objek matematik, struktur, teorem dan bukti supaya ia boleh diwakili, disahkan dan dikendalikan pada komputer, dengan itu memastikan ketepatan dan ketekalan kandungan matematik Perkembangan matematik dapat dikesan kembali ke akhir 19 dan awal abad ke-20, manakala matematik formal moden bermula dengan perkembangan logik matematik dan sains komputer pada abad ke-20. Matlamat utama matematik formal adalah untuk mewujudkan sistem formal, yang merangkumi satu set simbol, satu set aksiom asas dan satu set peraturan penaakulan ini, adalah mungkin untuk melaksanakan

Di. penghujung tahun lepas, Tao Zhexuan dan yang lain menggunakan Lean (sebuah teorem interaktif dan bahasa pengaturcaraan) memformalkan salah satu kertas kerja mereka. Kertas itu, bukti versi konjektur Freiman-Ruzsa polinomial, telah disiarkan di arXiv November lalu. Semasa menulis kod bahasa Lean, Tao Zhexuan juga menggunakan pembantu pengaturcaraan AI Copilot. Kejadian ini menarik perhatian meluas dalam komuniti matematik dan kecerdasan buatan.

Pada masa itu, Kevin Buzzard dari Imperial College London, penganjur terpenting komuniti sumber terbuka teknologi Lean, berkata: "Pada asasnya, jelas sekali apabila anda mendigitalkan sesuatu, anda boleh menggunakannya dengan cara baharu. Ia. Kami akan mendigitalkan matematik, yang akan menjadikan matematik lebih baik."

Profesor Buzzard ini ialah ahli matematik yang baru-baru ini mendakwa memformalkan bukti teorem terakhir Fermat, dan alat yang digunakannya juga Lean.

Dalam blog, beliau memperkenalkan latar belakang, motivasi dan kaedah khusus untuk melakukan ini.

Mengapa merasmikan bukti Teorem Terakhir Fermat?

Bentuk Teorem Terakhir Fermat adalah sangat mudah dan intuitif, tetapi membuktikannya amat sukar. Ini tidak diragukan lagi merupakan demonstrasi yang sangat baik tentang keindahan matematik yang mendalam. Sejak beberapa abad yang lalu, untuk menyelesaikan masalah ini, ahli matematik telah membangunkan dan menginovasi sejumlah besar teori matematik, yang mempunyai aplikasi dalam bidang dari kriptografi hingga fizik. Andrew Wiles mungkin telah diilhamkan oleh FLT, tetapi kerjanya sebenarnya membawa kepada kejayaan dalam Projek Langlands, satu siri idea yang meluas dalam matematik yang mengaitkan teori nombor, geometri algebra dan teori perwakilan kumpulan terkurang, dan akan tetap menarik perhatian ramai pada tahun 2024.

Secara sejarah, beberapa penemuan besar lain dalam teori nombor algebra (seperti teori pemfaktoran dalam medan nombor dan aritmetik dalam medan kitaran) sekurang-kurangnya sebahagiannya didorong oleh keinginan untuk pemahaman yang lebih mendalam tentang FLT.

Karya Wiles, dilengkapi dengan pelajarnya Richard Taylor, dibina di atas asas matematik abad ke-20 yang luas. Teknik asas yang diperkenalkan oleh Wiles - "teorem pengangkatan modulariti" - telah dipermudahkan secara konsep dan digeneralisasikan secara meluas dalam tempoh 30 tahun sejak kertas asal diterbitkan. Bidang ini masih sangat aktif sehingga kini. Kertas kerja Frank Calegari di Kongres Matematik Antarabangsa 2022, menggariskan kemajuan sejak kejayaan Wiles (lihat: https://arxiv.org/abs/2109.14145). Kevin Buzzard berkata bahawa aktiviti berterusan dalam bidang ini adalah salah satu motivasinya untuk memformalkan bukti FLT.

Pemformalisasian matematik, seni menukar matematik di atas kertas kepada bahasa pengaturcaraan komputer yang mampu memahami teorem dan membuktikan konsep. Bahasa pengaturcaraan ini, juga dikenali sebagai prover teorem interaktif (ITP), telah wujud selama beberapa dekad. Walau bagaimanapun, dalam beberapa tahun kebelakangan ini, bidang ini nampaknya telah menarik perhatian daripada komuniti matematik. Kami telah menyaksikan beberapa contoh pemformalkan penyelidikan dalam matematik, yang terbaru ialah pemformalkan pembuktian konjektur Freiman-Ruzsa polinomial oleh Terence Tao dan lain-lain. Kertas terobosan 2023 ini telah dirasmikan dalam Lean dalam masa tiga minggu sahaja. Kisah kejayaan sedemikian mungkin menyebabkan penonton berfikir bahawa ITP seperti Lean kini bersedia untuk memformalkan semua matematik moden.

Namun, kebenarannya jauh dari semudah itu. Dalam beberapa bidang matematik, seperti kombinatorik, kita dapat melihat beberapa kejayaan moden diformalkan dalam masa nyata. Bagaimanapun, Buzzard berkata beliau kerap menghadiri seminar teori nombor London dan sering menyedari bahawa pengetahuan Lean tentang definisi matematik moden tidak mencukupi untuk merumuskan keputusan yang diumumkan di seminar, apatah lagi mengesahkan buktinya.

Malah, "ketinggalan" teori nombor dalam aspek ini merupakan salah satu motivasi utama Buzzard untuk memulakan pemformalkan bukti kontemporari FLT. Menjelang akhir projek, Lean akan dapat memahami bentuk automorfik (kelas khas fungsi pembolehubah kompleks) dan perwakilan, perwakilan Galois, automorfisme terpendam, teorem promosi modulariti, aritmetik varieti algebra, teori medan kelas, Teorem dwi aritmetik , jenis Shimura dan konsep lain yang digunakan dalam teori nombor algebra moden. Pada pandangan Buzzard, dengan adanya asas ini, memformalkan apa yang berlaku dalam bidang kepakarannya sendiri bukan lagi fiksyen sains.

Jadi, kenapa awak buat macam ni? Buzzard menerangkan, "Jika kami percaya sesetengah saintis komputer, pertumbuhan eksponen dalam kecerdasan buatan akhirnya akan membolehkan komputer membantu ahli matematik dalam penyelidikan mereka. Kerja sedemikian boleh membantu komputer memahami perkara yang kami lakukan dalam penyelidikan matematik moden

Cara melaksanakan projek?

Projek pemformalkan Teorem Terakhir Fermat kini telah dilancarkan. Buzzard menunjukkan kemajuan semasa dalam grafik.

Penyelidik yang berminat boleh membaca butiran: https://imperialcollegelondon.github.io/FLT/blueprint/dep_graph_document.html

Projek ini dibiayai oleh EPSRC dan Buzzard akan menerima sokongan pembiayaan untuk lima tahun pertama. Dalam tempoh ini, matlamat pertamanya adalah untuk mengurangkan FLT kepada kenyataan yang diketahui oleh ahli matematik pada akhir 1980-an.

Sudah tentu, Buzzard tidak berniat untuk melakukan ini sendirian. Beliau berkata untuk beberapa bahagian hujah, beliau memahami prinsip asas tetapi tidak pernah meneliti butiran secara terperinci. Tambahan pula, Project Langlands turut memperkenalkan beberapa perkara penting, termasuk transformasi asas kitaran GL_2 dan Jacquet-Langlands. Pemahamannya tentang perkara-perkara yang mendalam ini tidak cukup mendalam.

Namun, inilah kelebihan projek formal. Buzzard akan dapat menyatakan hasil yang dia perlukan dalam Lean dan menyampaikannya kepada orang lain. Keindahan sistem ini ialah: anda tidak perlu memahami keseluruhan bukti FLT untuk menyumbang. Gambar rajah di atas memecahkan bukti kepada banyak lema kecil, menjadikannya sangat mudah untuk penyumberan ramai. Jika anda boleh membuktikan mana-mana lemma ini secara rasmi, Buzzard akan menunggu permintaan tarik anda.

Mereka yang ingin menyertai projek perlu tahu sesuatu tentang Lean. Untuk ini, Buzzard mengesyorkan buku teks dalam talian Matematik dalam Lean.

Pautan buku teks: https://leanprover-community.github.io/mathematics_in_lean/

Projek ini akan dijalankan pada aliran FLT dari sembang Lean Zulip, forum penyelidikan yang berkuasa untuk ahli matematik dan saintis komputer Bekerjasama dalam masa nyata, menerbitkan kod dan matematik dengan mudah, serta menggunakan sistem threading dan strim untuk menyokong berbilang perbualan bebas secara berkesan pada masa yang sama.

Pautan sembang Lean Zulip: https://leanprover.zulipchat.com/

Buzzard berkata dia tidak tahu berapa lama projek itu akan mengambil masa, tetapi dia pasti optimistik.

Pada masa yang sama, alat bukti formal seperti Lean juga sentiasa berulang. Berbanding dengan Lean yang asal, versi Lean 4 yang terkini mempunyai banyak pengoptimuman, termasuk pengkompil yang lebih pantas, pengendalian ralat yang lebih baik dan penyepaduan yang lebih baik dengan alatan luaran.

Pada penghujung tahun lalu, pasukan LeanDojo platform terbuka dan penyelidik dari Caltech turut melancarkan Lean Copilot, alat kerjasama yang direka untuk model bahasa besar untuk berinteraksi dengan manusia, menyuntik kuasa model AI yang besar ke dalam penyelidikan matematik.

"Saya meramalkan bahawa, jika digunakan dengan betul, AI akan menjadi pengarang bersama yang dipercayai dalam penyelidikan matematik dan banyak bidang lain menjelang 2026," kata Terence Tao dalam blog sebelum ini.

Saya harap ramalan Terence Tao akan menjadi kenyataan tidak lama lagi.

Bacaan berkaitan:

• 《Apakah bukti rasmi Terence Tao menggunakan AI? Fahami kehidupan masa lalu dan masa kini tekaan PFR dalam satu artikel》

• 《Pembantu bukti yang digemari Tao Zhexuan, Lean, menggunakan model besar》

• 《 membantu model Zhexuan menyelesaikan masalah model besar dan model Zhexuan Matematik adalah sangat penting Adakah ia menjadi disiplin pertama yang mencapai kejayaan dengan bantuan AI? 》

• 《Projek baharu Tao Zhexuan: membuktikan teorem nombor perdana dalam Lean, pelan tindakan penyelidikan sudah sedia》

^{pautan rujukan. strim /416277-FLT}

^{https://mp.weixin.qq.com/s/d9RSkRhlKH5ZMek3yTqe4Q}

Atas ialah kandungan terperinci Relay yang menjangkau lebih daripada 300 tahun: Diilhamkan oleh Terence Teru, ahli matematik memutuskan untuk menggunakan AI untuk memformalkan bukti Teorem Terakhir Fermat.. Untuk maklumat lanjut, sila ikut artikel berkaitan lain di laman web China PHP!