Bukti ditemukan oleh komputer

11

Pada tahun 1996, masalah terbuka lama diselesaikan oleh komputer; yaitu, bahwa aljabar Robbins dan aljabar Boolean adalah sama. Buktinya ditemukan oleh teorema teorema otomatis.

Selain itu, bukti teorema Four color yang diketahui mengandung komponen yang dihasilkan komputer.

Tujuan dari pertanyaan ini adalah untuk membuat daftar bukti yang (sepenuhnya atau sebagian) ditemukan oleh komputer (apakah hanya bukti yang diketahui atau yang ditemukan untuk pertama kali).

soft-question big-list proofs automated-theorem-proving Mahdi Cheraghchi
sumber
2
Beberapa grup sederhana terbatas sporadis (seperti grup Lyons pertama kali dibangun menggunakan komputer, yaitu, bukti keberadaan mereka (sebagian) dihasilkan oleh komputer.
jp
Pertanyaannya adalah "Teori Kompleksitas Eksperimental" yang digunakan untuk memecahkan masalah terbuka terkait dengan yang ini.
adrianN
IMHO Anda perlu membedakan lebih hati-hati antara "ditemukan" dan "diperiksa". Bukti Gonthier et al. Pasti tidak ditemukan oleh komputer.
gallais
1
pertanyaan yang bagus tapi sayangnya hampir setara dengan di mana & bagaimana komputer membantu membuktikannya
vzn
Juga sangat mirip: Apakah ada hasil yang sebelumnya tidak diketahui telah dibuktikan oleh teorema teorema otomatis? .
Petr Pudlák

Jawaban:

12

Contoh terkenal lainnya adalah bukti Hales tentang dugaan Kepler yang memiliki komponen pembantu komputer yang sangat besar.

Dari Wikipedia :

Pada Agustus 1998, Hales mengumumkan bahwa buktinya lengkap. Pada tahap itu terdiri dari 250 halaman catatan dan 3 gigabytes program komputer, data dan hasil.

Huck Bennett
sumber
10

Ini lebih merupakan jawaban meta karena ini adalah daftar daftar.

  1. Koran Doron Zeilberger . Dia adalah seorang ahli matematika dan komputernya terdaftar di rekan penulis Shalosh B. Ekhad di semua kertas di mana komputer berperan dalam mendapatkan hasil.

  2. Karya Georges Gonthier . Dia merekayasa bukti mesin-diperiksa dari teorema empat warna dan baru-baru ini bekerja pada teorema Feit-Thompson. Dia baru saja menyelesaikan formalisasi Teorema Ganjil.

  3. Arsip Bukti Resmi mengandung bukti yang diperiksa dengan Isabelle, dan termasuk teorema kebenaran untuk algoritma, teorema Gauss-Jordan, beberapa teori urutan, teori kategori, dan banyak lagi hasil klasik lainnya.

  4. Formalisasi 100 Teorema , berisi bukti yang diperiksa mesin dari beberapa teorema terkenal.

Vijay D
sumber
1
Terima kasih. Saya harus mengklarifikasi bahwa pertanyaan saya tidak berkaitan dengan bukti yang diverifikasi / divalidasi oleh komputer setelah penemuan, atau hasil di mana komputer memainkan peran untuk memperolehnya (tentu saja kita semua menggunakan komputer dalam penelitian kami, tetapi akhirnya berakhir dengan matematika mandiri bukti bahwa kita tidak bisa mengatakan telah "diturunkan" oleh komputer). Saya mencari dugaan yang buktinya dihasilkan (sebagian atau seluruhnya) oleh komputer.
Mahdi Cheraghchi