Cara menembak bukti Anda

Apa pedoman umum untuk memeriksa bukti Anda? Saya percaya ini penting bagi mahasiswa pascasarjana seperti saya. Saya sudah tahu apa yang perlu kita lakukan untuk membuktikan sesuatu, tetapi Anda harus selalu memeriksa semuanya sebelum mengirimkannya. Bahkan kepada penasihat Anda sendiri.

Saya telah mengembangkan sendiri beberapa strategi melalui coba-coba, dan mendapat banyak saran dari penasihat saya. Tapi ini selalu merupakan pekerjaan yang sangat membosankan. Biasanya, ketika Anda selesai dengan sesuatu, Anda hanya ingin melanjutkan ke masalah berikutnya, tetapi Anda masih harus tetap berpegang pada masalah saat ini sampai semuanya sempurna. Di sini saya menyajikan contoh daftar trik saya sendiri:

1. Isi rinciannya. Banyak kesalahan ada di tempat Anda menulis "sudah jelas bahwa ...", "tanpa kehilangan sifat umum ...", dll.
2. Coba beberapa angka. Coba kasus ekstrim, seperti "apa yang terjadi ketika saya menetapkan atau n = 1000 ".$n=1$$n=1000$
3. Simpan buku catatan yang bersih. Tuliskan setiap hari di atasnya, dan bandingkan dengan catatan kasar Anda. Saya mencoba menulis juga dalam lateks, saya menemukan banyak kesalahan dengan cara ini.

Apa strategi umum yang Anda terapkan untuk memeriksa bukti Anda?

Tujuan dari pertanyaan ini adalah menjadikannya komunitas-wiki.

Insinyur perangkat lunak memiliki gagasan yang mereka sebut " bau kode ". Ini adalah gejala dalam kode yang dapat mengindikasikan masalah yang lebih dalam. Insinyur perangkat lunak mengumpulkan daftar bau yang harus diwaspadai (yaitu metode yang terlalu panjang atau terlalu banyak parameter). Itu tidak selalu berarti ada masalah, tetapi hanya menunjukkan bahwa penulis mungkin ingin memeriksa ulang.

Saya mengusulkan bahwa kita juga harus mempertimbangkan "bukti bau" . Ini tidak akan memberi Anda algoritma untuk memeriksa bukti Anda, tetapi memberikan bahasa dan metafora untuk mengenali kemungkinan masalah dalam bukti. Beberapa contoh bukti berbau:

1. Kata keterangan "Jelas", "Jelas", dll.
2. Referensi ke bukti hasil sebelumnya dan bukan referensi ke hasil itu sendiri.
3. Penggunaan hasil yang sembrono dengan banyak prasyarat teknis.

Ada juga aroma yang lebih halus. Misalnya, jika bukti menggunakan teorema binomial untuk memperluas ekspresi dan kemudian menggunakan teorema binomial untuk kembali ke bentuk tertutup, maka mungkin ada manipulasi langsung pada formulir tertutup yang memberikan hasil yang sama.

Saran saya adalah untuk mengumpulkan (bau atau tertulis) daftar bau tersebut dan memeriksanya saat Anda membaca pekerjaan Anda. Efek samping yang bagus dari pendekatan ini adalah bahwa itu juga akan membuat Anda menjadi pembaca yang lebih baik.

Catatan: Harapan saya dalam jawaban ini adalah memberikan sisi intuitif pada jawaban keras yang diberikan oleh How to Write a Proof Lamport yang dirujuk dalam jawaban M. Alaggan.

Ada makalah yang sangat bagus oleh Leslie Lamport ( Cara menulis bukti ). Ini sebenarnya adalah proposal olehnya tentang gaya penulisan bukti terperinci sedemikian rupa sehingga:

(1) Memungkinkan mendeteksi kesalahan secara langsung

(2) Jelaskan asumsi dan teorema mana yang digunakan di bagian mana, yang membuatnya cukup mudah untuk melihat apa yang terjadi jika Anda ingin (misalnya) menggunakan asumsi yang lebih lemah

Ada juga beberapa pengalaman komunitas dan komentar yang menginspirasi tentang teknik ini pada MO yang menunjukkan pengalaman positif secara umum (dan beberapa sumber daya lainnya juga).

Pembaruan: ada versi baru Cara menulis bukti abad ke-21 .

Dick Lipton memiliki artikel bagus berjudul ' Cara Membuktikan Bukti adalah Bukti '

Sepertinya saya ingat pernah membaca akun populer dulu tentang bagaimana fisikawan menangani masalah analog. Siapa yang tahu seberapa akurat versi berikut ini; koreksi dipersilahkan. Tetapi saya menemukan strategi yang mendasarinya cukup luar biasa.

Mereka menjelaskan bagaimana mereka bisa percaya pada lubang hitam. Lubang hitam pada awalnya murni konstruksi matematika, seperti benda aneh lainnya dalam fisika seperti lubang cacing. Strategi mereka sangat mengejutkan: mereka secara matematis akan melemparkan benda lain ke objek yang akan diuji. Lubang cacing gagal tes mereka karena mereka menemukan bahwa lubang cacing akan runtuh bahkan di hadapan benda fisik yang normal, mungkin asteroid. Tapi lubang hitam lulus tes ini: lubang hitam akan bertahan dengan dilemparkannya asteroid ke dalamnya. Jadi mereka mencoba melemparkan bintang padanya. Hasil yang sama Akhirnya, mereka melemparkan lubang hitam lain ke lubang hitam itu dan selamat. Sebagai hasil dari ini, mereka tumbuh cukup percaya diri dalam keberadaan lubang hitam untuk benar-benar mulai mencari mereka di alam semesta yang sebenarnya.

Jadi relevansi dan penerapan strategi di atas adalah untuk mulai melempar barang pada bukti Anda. Apakah itu lolos dari pemeriksaan kewarasan ? Jika Anda menghapus asumsi yang diperlukan, apakah itu runtuh seperti seharusnya? Apakah itu runtuh seperti seharusnya ketika diterapkan pada kasus di luar ruang lingkupnya? Apakah itu tahan generalisasi dan spesialisasi yang masuk akal? Lihat daftar heuristik di Polya's How to Solve It . Coba mutasikan bukti Anda dengan heuristik ini dan lihat apakah itu berdiri dan jatuh sebagaimana mestinya.

Saya pikir salah satu pendekatan teraman adalah dengan menghadirkan banyak bukti independen. Maka Anda dapat yakin bahwa hasil utama Anda benar, bahkan jika Anda memiliki kesalahan dalam beberapa detail bukti.

Salah satu teknik yang menurut saya bermanfaat adalah memikirkan hasil apa lagi yang bisa dibuktikan oleh strategi pembuktian. Jika saya dapat dengan mudah mengadaptasi strategi bukti untuk membuktikan masalah terbuka besar atau bahkan masalah yang tidak terbuka tetapi memiliki solusi yang terlalu rumit dibandingkan dengan kompleksitas strategi bukti, maka itu adalah alasan besar untuk ragu bukti.

Saya selalu memeriksa ulang bukti saya dengan pemeriksa bukti seperti COQ atau ISABELLE . Jika Anda dapat membuktikan bukti dalam bahasa pemrograman ini, Anda dapat memastikan bukti Anda benar. Sesederhana istilah lambda;).