- Lean adalah bahasa pemrograman yang dirancang untuk memformalkan matematika, sehingga memungkinkan matematikawan memperlakukan teorema matematika seperti kode
- Pengguna menulis teorema, bukti, aksioma dalam bentuk kode, dan proses pembuktian dilakukan melalui kumpulan perintah bernama tactic
- Meskipun bukti belum benar-benar diselesaikan, kita dapat menutupnya sementara dengan
sorry; ini adalah bukti semu yang mirip dengan any di TypeScript
- Jika menambahkan aksioma yang salah (misalnya
2 = 3), maka muncul risiko kontradiksi logis dan kemungkinan membuktikan setiap klaim
- Karena Lean hanya menghasilkan kesimpulan atas dasar aksioma yang dipilih dan sistem pembuktian yang logis, menjaga validitas matematika menjadi sangat penting
Lean: Matematika seperti kode
- Lean adalah bahasa pemrograman yang dibuat khusus untuk menulis matematika yang terformal
- Melalui Lean, para matematikawan dapat mengekspresikan matematika dalam bentuk kode dan mengatur teorema serta bukti mereka agar dapat berkolaborasi dan berbagi
- Ini menggambarkan masa depan di mana pengetahuan matematika manusia dalam jumlah besar akan bisa diverifikasi dan dikomposisi secara mekanis dalam bentuk kode
Langkah pertama dalam membuktikan dengan Lean
- Bentuk
theorem two_eq_two : 2 = 2 := by sorry memungkinkan deklarasi teorema sederhana di Lean
- Saat bukti belum selesai,
sorry dapat dimasukkan, tetapi ini hanya solusi sementara, bukan bukti yang sebenarnya
sorry lolos pemeriksaan verifikasi bukti Lean, namun tidak dapat dipercaya secara logis
- Untuk bukti yang lengkap, digunakan tactic seperti
rfl (reflexivity) untuk membuktikan persamaan yang jelas seperti 2 = 2
- Bagian yang sudah terbukti dapat digunakan kembali di teorema lain menggunakan
exact, sehingga menekankan modularitas
Aksioma dan kontradiksi: ketika matematika dianggap berhantu
- Jika menambahkan aksioma seperti
axiom math_is_haunted : 2 = 3, Lean akan menganggapnya benar
- Aksioma ini dapat dipakai dalam proses pembuktian berikutnya, hingga memungkinkan pembuktian simpulan yang tidak masuk akal secara matematika, misalnya
2 + 2 = 6
- Dengan tactic
rewrite, 2 bisa diganti menjadi 3 dan proses pembuktian persamaan dapat diselesaikan dengan rfl
- Bila kontradiksi dipicu oleh aksioma yang tidak tepat, di Lean juga terjadi keadaan setiap proposisi dapat dibuktikan (keruntuhan logis)
- Pada awal abad ke-20, kontradiksi dalam sistem aksioma seperti Paradoks Russell memicu refleksi mendasar dalam matematika
- Dengan demikian, Lean menunjukkan bahwa pemilihan aksioma sangat menentukan dalam menjaga kewajaran sistem logika
Lean sebagai proof checker
- Jika aksioma dipilih dengan tepat dan Lean secara logis benar, maka akan menghasilkan kesimpulan dengan keandalan teoritis
- Dari persamaan sederhana hingga teorema yang sangat kompleks (misalnya Fermat's Last Theorem), semuanya diverifikasi dengan prinsip yang sama
- Teorema besar dibangun sebagai akumulasi bukti berulang dari teorema dan substruktur, sehingga keseluruhan strukturnya terbentuk secara bertingkat
- Sebagai contoh, proyek skala besar untuk memformalkan Fermat's Last Theorem di Lean sedang berjalan, dan akhirnya diharapkan terselesaikan sistem bukti formal tanpa
sorry
Kenikmatan mempelajari Lean
- Pembuktian dengan Lean adalah perpaduan kreatif antara pemrograman dan matematika
- Mulai dari cara membuktikan proposisi sederhana, hingga bertahap membangun matematika yang lebih kompleks dan mendalam secara ketat, itulah kenikmatan utamanya
- Materi tutorial resmi dan komunitas (seperti Natural Numbers Game, Mathematics in Lean, dan lainnya) sangat cocok untuk pemula
- Dengan Lean, Anda memformalkan logika secara langsung dan bisa menemukan kembali keindahan ide serta argumen yang cerdik
- Pada akhirnya, artikel menyimpulkan bahwa tanpa alasan apa pun, bagi jenis orang tertentu, Lean menghadirkan kesenangan yang khas
Belum ada komentar.