Mengapa begitu sulit bagi komputer untuk membuktikan sesuatu?

Ini mungkin dianggap pertanyaan bodoh. Saya bukan jurusan ilmu komputer (dan saya juga belum jurusan matematika), jadi tolong permisi jika Anda berpikir bahwa pertanyaan-pertanyaan berikut menampilkan beberapa asumsi salah besar.

Walaupun ada rencana untuk memformalkan Teorema Terakhir Fermat (lihat presentasi ini ), saya belum pernah membaca atau mendengar bahwa komputer dapat membuktikan bahkan sebuah teorema "sederhana" seperti Pythagoras '.

Kenapa tidak? Apakah kesulitan utama di balik pembuatan bukti yang sepenuhnya otonom oleh komputer, hanya dibantu oleh beberapa "aksioma bawaan"?

Pertanyaan kedua yang ingin saya tanyakan adalah sebagai berikut: Mengapa kita dapat memformalkan banyak bukti, sementara saat ini mustahil bagi komputer untuk membuktikan teorema sendiri? Mengapa itu "lebih sulit"?

Walaupun ada rencana untuk memformalkan Teorema Terakhir Fermat (lihat presentasi ini), saya belum pernah membaca atau mendengar bahwa komputer dapat membuktikan bahkan sebuah teorema "sederhana" seperti Pythagoras '.

Pada tahun 1949 Tarski membuktikan bahwa hampir semua yang ada di The Elements terletak di dalam fragmen logika yang dapat diputuskan, ketika ia menunjukkan kepastian teori orde pertama dari bidang tertutup nyata. Jadi teorema Pythagoras khususnya tidak banyak dibicarakan karena tidak terlalu sulit.

Secara umum, hal yang membuat teorema terbukti sulit adalah induksi. Logika orde pertama tanpa induksi memiliki properti yang sangat berguna yang disebut properti subformula: formula yang benar memiliki bukti hanya melibatkan sub istilah dari . Ini berarti bahwa mungkin untuk membangun pembuktian teorema yang dapat memutuskan apa yang akan dibuktikan selanjutnya berdasarkan analisis teorema yang mereka perintahkan untuk buktikan. (Instansiasi Quantifier dapat membuat gagasan subformula yang tepat sedikit lebih halus, tetapi kami memiliki teknik yang masuk akal untuk mengatasi hal ini.)$A$$A$

Namun, penambahan skema induksi pada aksioma merusak properti ini. Satu-satunya bukti formula yang benar mungkin memerlukan melakukan bukti yang tidak sintaksis suatu subformula dari . Ketika kita menemukan ini dalam sebuah makalah bukti, kita mengatakan kita harus "memperkuat hipotesis induksi". Ini cukup sulit dilakukan oleh komputer, karena penguatan yang tepat dapat memerlukan informasi spesifik domain yang signifikan, dan pemahaman tentang mengapa Anda membuktikan teorema tertentu. Tanpa informasi ini, generalisasi yang benar-benar relevan dapat hilang di hutan yang tidak relevan.B $A$$B$$A$

Dua kesulitan utama. Ketidaklengkapan (lihat Teorema Ketidaklengkapan Gödel) dan luasnya ruang pencarian (ada teorema yang jauh lebih menarik daripada yang menarik). Kemajuan yang cukup besar telah dibuat dengan menggunakan asisten bukti ( Coq , Isabelle, Agda, dll). Dengan ini, ahli matematika menulis teorema dan lemma dan asisten pembuktian membantu menemukan bukti dan memastikan bahwa bukti tersebut valid secara logis.

$P$$Q$$P\wedge Q$

Makalah ini menjelaskan bagaimana asisten bukti Coq digunakan untuk membuktikan teorema empat warna. Matematika mekanis ( ikhtisar ) adalah salah satu area TCS yang dikhususkan untuk (semi) teorema pembuktian otomatis (dan secara umum menggunakan komputer untuk membantu ahli matematika).

Satu area di mana pembuktian teorema otomatis (sejenis) membuat dampak adalah dalam pengecekan model dan pencarian model. Pemeriksaan model berkaitan dengan menentukan apakah sistem yang diberikan memenuhi properti yang diberikan, sedangkan penemuan model menemukan sistem untuk memenuhi koleksi properti yang diberikan. Alat Paduan menggunakan pengecekan model dan penemuan model untuk efek yang baik, dan itu cukup bermanfaat.