Di mana dan bagaimana komputer membantu membuktikan teorema?

Tujuan dari pertanyaan ini adalah untuk mengumpulkan contoh-contoh dari ilmu komputer teoretis di mana penggunaan komputer secara sistematis sangat membantu

1. dalam membangun dugaan yang mengarah pada teorema,
2. memalsukan pendekatan dugaan atau bukti,
3. membangun / memverifikasi (bagian dari) bukti.

Jika Anda memiliki contoh spesifik, tolong jelaskan bagaimana itu dilakukan. Mungkin ini akan membantu orang lain menggunakan komputer secara lebih efektif dalam penelitian sehari-hari mereka (yang tampaknya masih menjadi praktik yang tidak biasa di TCS sampai hari ini).

(Ditandai sebagai komunitas wiki, karena tidak ada jawaban "benar" tunggal.)

Contoh yang sangat terkenal adalah Teorema Empat Warna , yang awalnya dibuktikan dengan pemeriksaan lengkap.

Perbaiki poin di pesawat. Biarkan T menjadi triangulasi (yaitu grafik garis lurus planar dengan titik-titik sebagai simpul yang sepenuhnya triangulasi), dan biarkan bobot triangulasi menjadi jumlah dari panjang sisi.$n$

Menunjukkan bahwa masalah triangulasi berat minimum (MWT) adalah NP-hard adalah masalah yang sudah lama berdiri, dipersulit oleh kenyataan bahwa panjang tepi melibatkan akar kuadrat, dan presisi yang diinginkan yang dibutuhkan untuk menghitungnya secara akurat sulit untuk diikat.

Mulzer dan Rote menunjukkan bahwa MWT adalah NP-hard , dan dalam prosesnya menggunakan bantuan komputer untuk memverifikasi kebenaran gadget mereka. Sejauh yang saya tahu, tidak ada bukti alternatif.

Bukti Thomas Hales (situsnya, MathSciNet ) dari dugaan Kepler melibatkan begitu banyak analisis kasus - dan kasus-kasus itu pada gilirannya diverifikasi oleh komputer - sehingga ia memutuskan untuk mencoba bukti formal dari itu. Proyeknya untuk melakukannya adalah FlysPecK , dan dia memperkirakan itu akan memakan waktu 20 tahun kerja.

Peneliti dalam Bahasa Pemrograman secara teratur menggunakan bukti yang dibantu komputer dalam pekerjaan mereka, meskipun saya tidak tahu betapa pentingnya hal ini dalam hal proses penelitian mereka (tentu saja membuat mereka tidak harus menulis banyak manipulasi yang membosankan, meskipun).

Doron Zeilberger telah melakukan beberapa pekerjaan di bidang bukti yang dihasilkan komputer. Terutama, ia telah menyiapkan program Maple untuk membuktikan identitas geometris , dan program lain untuk membuktikan kelas identitas kombinatorial . Beberapa metode yang disebutkan dalam buku A = B .

Komputer juga telah digunakan untuk menentukan batas atas pada waktu berjalannya program backtracking memecahkan masalah NP-hard, dan membangun gadget untuk membuktikan hasil yang tidak dapat diperkirakan. Topik ini dan topik-topik menyenangkan lainnya menanti Anda dalam esai singkat (peringatan, promosi diri ekstrem di depan) berjudul "Menerapkan Praktek Ke Teori." Lihat http://arxiv.org/abs/0811.1305

Dengan daftar yang bagus ini, sepertinya saya harus memperbarui makalah!

Contoh tandingan terhadap dugaan Hirsch , penting untuk pemrograman linier dan kombinatorik polihedral, diusulkan oleh Francisco Santos baru-baru ini. Verifikasi komputer digunakan pertama kali untuk menetapkan beberapa properti yang diperlukan dari contoh, meskipun argumen tanpa bantuan kekuatan komputasi ditemukan setelahnya, lih. Posting blog Gil Kalai atau tulisan di arxiv .

Belum pernah melihat ini disebutkan di sini, tetapi teorema teorema otomatis memecahkan masalah terbuka lama apakah Robbins algebas adalah boolean:

http://www.cs.unm.edu/~mccune/papers/robbins/

Ini terutama penting karena komputer mengembangkan seluruh bukti dan masalahnya telah terbuka selama beberapa dekade.

Tidak sepenuhnya yakin apakah itu memenuhi syarat sebagai TCS, tetapi bisa dibilang itu terkait erat.

The algoritma Karloff-Zwick untuk MAX-3SAT diperbaiki sehingga diharapkan kinerja 7/8. Namun analisis ini bergantung pada ketidaksetaraan volume bola yang tidak terbukti. Ketidaksetaraan ini akhirnya dikonfirmasi melalui bukti yang dibantu komputer dalam makalah Zwick yang lain .

Selain bukti Hales terhadap dugaan Kepler sebagaimana disebutkan di atas, bukti dugaan Honeycomb dan bukti dugaan Dodecahedral juga dibantu oleh komputer.

Anda dapat memeriksa Shalosh B. ekhad ini homepage . Komputer ini telah menerbitkan makalah untuk sementara waktu (biasanya dengan penulis bersama).

Christian Urban menggunakan asisten bukti Isabelle untuk memeriksa salah satu teorema utama dalam tesis PhD-nya sebenarnya adalah teorema [1]. Menggunakan asisten, beberapa perubahan perlu dilakukan, tetapi hasilnya cukup banyak berdiri.

Demikian pula, Urban dan Narboux juga menemukan kesalahan dalam bukti pena dan kertas bukti kelengkapan Crary untuk pemeriksaan kesetaraan.

Meikle dan Fleuriot memformalkan Grundlagen Hilbert di Isabelle dan menunjukkan bahwa, bertentangan dengan klaim Hilbert, ia masih mengandalkan intutisinya untuk memformalkan geometri secara aksiomatis (IIRC ada lubang dalam buktinya yang berasal dari Hilbert dengan asumsi hal-hal tentang diagram) [3] .

[1]: Meninjau Kembali Cut-Elimination: Satu Bukti Sulit Benar-Benar Bukti

[2]: Formalisasi dalam Bukti Kelengkapan Nominal Isabelle Crary untuk Memeriksa Kesetaraan

[3]: Memformalkan Grundlagen Hilbert di Isabelle / Isar

Hasil dalam " Geometri Pohon Pencarian Biner " oleh Demaine, Harmon, Iacono, Kane, dan Patraşcu dikembangkan dengan bantuan perangkat lunak untuk menguji berbagai skema pengisian daya dan membangun penilaian optimal untuk urutan akses kecil. (Dan ya, "menilai" adalah istilah yang benar.)

N. Shankar memverifikasi (sepenuhnya dan secara mekanis) bukti Godel tentang teorema ketidaklengkapan dan Gereja - teorema Rosser menggunakan pepatah teorema Boyer - Moore. Ada sebuah buku yang menjelaskan bagaimana hal itu dilakukan.

Rumus untuk algoritma Bailey-Borwein-Plouffe untuk menghitung bit n Pi tanpa menghitung bit yang lebih signifikan ditemukan, menurut Simon Plouffe , menggunakan sistem bukti komputer.

Ada banyak contoh dalam analisis algoritma kasus rata-rata. Mungkin beberapa yang paling awal adalah eksperimen komputer yang mengarah ke kertas "Beberapa hasil perilaku yang tidak terduga diharapkan untuk pengemasan bin" oleh Bentley, Johnson, Leighton, McGeoch dan McGeoch dalam STOC 1984.