1. Pendahuluan

1.1. Memulai

Tujuan buku ini adalah mengajarkan cara memformalkan matematika menggunakan asisten pembuktian interaktif Lean 4. Buku ini mengasumsikan bahwa Anda memahami sejumlah matematika, tetapi tidak menuntut banyak prasyarat. Meskipun contoh-contoh yang dibahas berkisar dari teori bilangan hingga teori ukuran dan analisis, kita akan berfokus pada aspek-aspek dasar bidang tersebut. Dengan demikian, jika bidang-bidang itu belum akrab bagi Anda, Anda dapat mempelajarinya sambil berjalan. Kami juga tidak mengasumsikan pengalaman sebelumnya dengan metode formal. Formalisasi dapat dipandang sebagai sejenis pemrograman komputer: kita akan menulis definisi, teorema, dan bukti matematika dalam bahasa yang teratur, layaknya bahasa pemrograman, yang dapat dipahami Lean. Sebagai gantinya, Lean memberikan umpan balik dan informasi, menafsirkan ekspresi serta menjamin bahwa ekspresi itu terbentuk dengan baik, dan pada akhirnya mengesahkan kebenaran bukti kita.

Anda dapat mempelajari Lean lebih lanjut melalui laman proyek Lean dan laman web komunitas Lean. Tutorial ini menggunakan pustaka Lean yang besar dan terus berkembang, Mathlib. Jika belum bergabung, kami juga sangat menyarankan Anda untuk bergabung dengan grup obrolan daring Lean di Zulip. Di sana Anda akan menemukan komunitas penggemar Lean yang aktif dan ramah, yang dengan senang hati menjawab pertanyaan dan memberikan dukungan moril.

Walaupun versi PDF atau HTML buku ini dapat dibaca secara daring, buku ini dirancang untuk dibaca secara interaktif dengan menjalankan Lean dari dalam editor VS Code. Untuk memulai:

  1. Pasang Lean 4 dan VS Code dengan mengikuti petunjuk pemasangan ini.

  2. Ambil repositori dengan mengeklik simbol forall (∀) di sudut kanan atas VS Code, lalu pilih Open Project, Download Project, dan Mathematics in Lean.

  3. Setiap bagian buku ini memiliki berkas Lean terkait yang berisi contoh dan latihan. Berkas-berkas tersebut terdapat di folder MIL dan disusun menurut bab. Kami sangat menyarankan agar Anda membuat salinan folder itu, lalu bereksperimen dan mengerjakan latihan di dalam salinan tersebut. Dengan demikian, berkas asli tetap utuh dan repositori juga lebih mudah diperbarui ketika berubah (lihat di bawah). Anda dapat menamai salinan itu my_files atau nama lain yang Anda inginkan, dan menggunakannya untuk membuat berkas Lean Anda sendiri.

Setelah itu, Anda dapat membuka buku ajar ini di panel samping VS Code sebagai berikut:

  1. Tekan ctrl-shift-P (command-shift-P di macOS).

  2. Ketik Lean 4: Docs: Show Documentation Resources pada bilah yang muncul, lalu tekan return. (Anda dapat langsung menekan return untuk memilihnya begitu perintah itu disorot dalam menu.)

  3. Pada jendela yang terbuka, klik Mathematics in Lean.

Sebagai alternatif, Anda dapat menjalankan Lean dan VS Code di awan menggunakan Codespaces. Petunjuknya tersedia di laman proyek Mathematics in Lean di GitHub. Kami tetap menyarankan agar Anda bekerja dalam salinan folder MIL, seperti dijelaskan di atas.

Buku ajar ini dan repositori yang menyertainya masih dalam pengembangan. Anda dapat memperbarui repositori dengan mengetik git pull, lalu lake exe cache get di dalam folder mathematics_in_lean. (Langkah ini mengasumsikan bahwa Anda belum mengubah isi folder MIL; itulah sebabnya kami menyarankan agar Anda membuat salinan.)

Sambil membaca buku ajar yang berisi penjelasan, petunjuk, dan anjuran, Anda diharapkan mengerjakan latihan dalam folder MIL. Teks buku akan sering memuat contoh seperti berikut:

#eval "Hello, World!"

Anda seharusnya dapat menemukan contoh yang sama dalam berkas Lean terkait. Jika Anda mengeklik baris tersebut, VS Code akan menampilkan umpan balik Lean di jendela Lean InfoView. Jika penunjuk diarahkan ke perintah #eval, VS Code akan menampilkan tanggapan Lean terhadap perintah itu dalam jendela sembul. Silakan ubah berkas tersebut dan coba contoh buatan Anda sendiri.

Buku ini juga menyediakan banyak latihan menantang untuk Anda coba. Jangan terburu-buru melewatinya! Lean adalah tentang melakukan matematika secara interaktif, bukan sekadar membacanya. Mengerjakan latihan merupakan bagian utama dari pengalaman belajar ini. Anda tidak harus mengerjakan semuanya; apabila Anda merasa sudah menguasai keterampilan terkait, silakan lanjut ke bagian berikutnya. Anda selalu dapat membandingkan penyelesaian Anda dengan penyelesaian dalam folder solutions yang terkait dengan setiap bagian.

1.2. Ikhtisar

Sederhananya, Lean adalah alat untuk menyusun ekspresi kompleks dalam bahasa formal yang dikenal sebagai teori tipe dependen.

Setiap ekspresi memiliki sebuah tipe, dan Anda dapat menggunakan perintah #check untuk menampilkannya. Beberapa ekspresi memiliki tipe seperti ℕ atau ℕ → ℕ. Ekspresi-ekspresi ini merupakan objek matematika.

#check 2 + 2

def f (x : ℕ) :=
  x + 3

#check f

Beberapa ekspresi bertipe Prop. Ekspresi-ekspresi ini merupakan pernyataan matematika.

#check 2 + 2 = 4

def FermatLastTheorem :=
  ∀ x y z n : ℕ, n > 2 ∧ x * y * z ≠ 0 → x ^ n + y ^ n ≠ z ^ n

#check FermatLastTheorem

Beberapa ekspresi memiliki suatu tipe P, sedangkan P sendiri bertipe Prop. Ekspresi semacam itu merupakan bukti bagi proposisi P.

theorem easy : 2 + 2 = 4 :=
  rfl

#check easy

theorem hard : FermatLastTheorem :=
  sorry

#check hard

Jika Anda berhasil menyusun ekspresi bertipe FermatLastTheorem dan Lean menerimanya sebagai term dengan tipe tersebut, Anda telah melakukan sesuatu yang sangat mengesankan. (Menggunakan sorry berarti berbuat curang, dan Lean mengetahuinya.) Sekarang Anda sudah memahami permainannya. Yang tersisa hanyalah mempelajari aturannya.

Buku ini melengkapi tutorial pendamping, Theorem Proving in Lean, yang memberikan pengantar lebih menyeluruh tentang kerangka logika yang mendasari Lean serta sintaks intinya. Theorem Proving in Lean ditujukan bagi orang yang lebih suka membaca buku petunjuk dari awal sampai akhir sebelum menggunakan mesin pencuci piring baru. Jika Anda termasuk orang yang lebih suka langsung menekan tombol start, lalu baru mencari tahu cara mengaktifkan fitur penggosok panci, lebih masuk akal untuk memulai dari sini dan merujuk kembali ke Theorem Proving in Lean ketika diperlukan.

Hal lain yang membedakan Matematika dalam Lean dari Theorem Proving in Lean adalah penekanan yang jauh lebih besar pada penggunaan taktik di buku ini. Karena kita berusaha menyusun ekspresi yang kompleks, Lean menawarkan dua cara untuk melakukannya: kita dapat menuliskan ekspresi itu sendiri (tepatnya, deskripsi tekstual yang sesuai), atau kita dapat memberi Lean instruksi untuk menyusunnya. Sebagai contoh, ekspresi berikut merepresentasikan bukti atas fakta bahwa jika n genap, maka m * n juga genap:

example : ∀ m n : Nat, Even n → Even (m * n) := fun m n ⟨k, (hk : n = k + k)⟩ ↦
  have hmn : m * n = m * k + m * k := by rw [hk, mul_add]
  show ∃ l, m * n = l + l from ⟨_, hmn⟩

Term bukti tersebut dapat dipadatkan menjadi satu baris:

example : ∀ m n : Nat, Even n → Even (m * n) :=
fun m n ⟨k, hk⟩ ↦ ⟨m * k, by rw [hk, mul_add]⟩

Sebaliknya, berikut ini adalah bukti bergaya taktik untuk teorema yang sama; baris yang diawali dengan -- merupakan komentar sehingga diabaikan oleh Lean:

example : ∀ m n : Nat, Even n → Even (m * n) := by
  -- Misalkan `m` dan `n` bilangan asli, dan asumsikan `n = 2 * k`.
  rintro m n ⟨k, hk⟩
  -- Kita perlu membuktikan bahwa `m * n` dua kali suatu bilangan asli.
  -- Mari tunjukkan bahwa nilainya dua kali `m * k`.
  use m * k
  -- Substitusikan `n`,
  rw [hk]
  -- dan sekarang hasilnya jelas.
  ring

Saat Anda memasukkan setiap baris bukti semacam itu di VS Code, Lean menampilkan keadaan bukti di jendela terpisah, yang memberi tahu fakta-fakta yang sudah Anda tetapkan dan tugas-tugas yang masih harus diselesaikan untuk membuktikan teorema tersebut. Anda dapat memutar ulang bukti dengan menelusuri baris demi baris, karena Lean akan terus menampilkan keadaan bukti pada posisi kursor. Dalam contoh ini, Anda akan melihat bahwa baris pertama bukti memperkenalkan m dan n (pada tahap itu kita dapat mengganti nama keduanya jika menginginkannya), serta menguraikan hipotesis Even n menjadi suatu k dan asumsi bahwa n = 2 * k. Baris kedua, use m * k, menyatakan bahwa kita akan menunjukkan m * n genap dengan membuktikan m * n = 2 * (m * k). Baris berikutnya menggunakan taktik rw untuk mengganti n dengan 2 * k dalam sasaran (rw adalah singkatan dari rewrite, “tulis ulang”), sedangkan taktik ring menyelesaikan sasaran yang dihasilkan, yakni m * (2 * k) = 2 * (m * k).

Kemampuan menyusun bukti dalam langkah-langkah kecil dengan umpan balik bertahap sangatlah berdaya guna. Oleh karena itu, bukti taktik sering kali lebih mudah dan lebih cepat ditulis daripada term bukti. Tidak ada batas tegas di antara keduanya: bukti taktik dapat disisipkan ke dalam term bukti, seperti yang kita lakukan dengan frasa by rw [hk, mul_add] pada contoh di atas. Kita juga akan melihat bahwa, sebaliknya, menyisipkan term bukti pendek di tengah bukti taktik sering kali berguna. Meskipun demikian, buku ini akan menekankan penggunaan taktik.

Dalam contoh kita, bukti taktik tersebut juga dapat dipadatkan menjadi satu baris:

example : ∀ m n : Nat, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩; use m * k; rw [hk]; ring

Di sini kita menggunakan taktik untuk menjalankan langkah-langkah bukti yang kecil. Namun, taktik juga dapat menyediakan otomatisasi yang cukup besar, serta membenarkan perhitungan yang lebih panjang dan langkah inferensi yang lebih besar. Sebagai contoh, kita dapat memanggil penyederhana Lean dengan aturan khusus untuk menyederhanakan pernyataan tentang paritas sehingga teorema kita terbukti secara otomatis.

example : ∀ m n : Nat, Even n → Even (m * n) := by
  intros; simp [*, parity_simps]

Perbedaan besar lainnya di antara kedua pengantar tersebut adalah bahwa Theorem Proving in Lean hanya bergantung pada inti Lean dan taktik bawaannya, sedangkan Matematika dalam Lean dibangun di atas pustaka Lean yang kuat dan terus berkembang, Mathlib. Dengan demikian, kami dapat menunjukkan cara menggunakan sejumlah objek dan teorema matematika di dalam pustaka tersebut, serta beberapa taktik yang sangat berguna. Buku ini tidak dimaksudkan sebagai ikhtisar lengkap pustaka tersebut; laman web komunitas menyediakan dokumentasi yang luas. Sebaliknya, tujuan kami adalah memperkenalkan gaya berpikir yang mendasari formalisasi itu dan menunjukkan sejumlah titik masuk dasar, agar Anda merasa nyaman menjelajahi pustaka dan menemukan berbagai hal secara mandiri.

Pembuktian teorema interaktif dapat membuat frustrasi, dan kurva belajarnya terjal. Namun, komunitas Lean sangat ramah kepada pendatang baru, dan orang-orang selalu tersedia di grup obrolan Lean di Zulip untuk menjawab pertanyaan. Kami berharap dapat berjumpa dengan Anda di sana, dan kami yakin bahwa tak lama lagi Anda pun akan mampu menjawab pertanyaan semacam itu serta berkontribusi pada pengembangan Mathlib.

Jadi, inilah misi Anda, jika Anda bersedia menerimanya: terjunlah, cobalah latihan-latihannya, ajukan pertanyaan di Zulip, dan bersenang-senanglah. Namun, Anda sudah diperingatkan: pembuktian teorema interaktif akan menantang Anda untuk memikirkan matematika dan penalaran matematika dengan cara-cara yang sama sekali baru. Hidup Anda mungkin tidak akan pernah sama lagi.

Ucapan terima kasih. Kami berterima kasih kepada Gabriel Ebner karena telah menyiapkan infrastruktur untuk menjalankan tutorial ini di VS Code, serta kepada Kim Morrison dan Mario Carneiro atas bantuan mereka dalam memindahkannya dari Lean 3 ke Lean 4. Kami juga berterima kasih atas bantuan dan koreksi dari Takeshi Abe, Julian Berman, Alex Best, Axel Boldt, Thomas Browning, Bulwi Cha, Hanson Char, Bryan Gin-ge Chen, Steven Clontz, Mauricio Collaris, Johan Commelin, Mark Czubin, Alexandru Duca, Pierpaolo Frasa, Denis Gorbachev, Winston de Greef, Darij Grinberg, Mathieu Guay-Paquet, Rik Heurter, Marc Huisinga, Benjamin Jones, Julian Külshammer, Victor Liu, Jimmy Lu, Martin C. Martin, Giovanni Mascellani, John McDowell, Joseph McKinsey, Bhavik Mehta, Sebastian Miele, Isaiah Mindich, Kabelo Moiloa, Hunter Monroe, Pietro Monticone, Oliver Nash, Emanuelle Natale, Filippo A. E. Nuccio, Pim Otte, Nicolas Rolland, Keith Rush, Yannick Seurin, Guilherme Silva, Bernardo Subercaseaux, Pedro Sánchez Terraf, Matthew Toohey, Alistair Tucker, Floris van Doorn, Veniamin Viflyantsev, Eric Wieser, dan kontributor lainnya. Karya kami mendapat sebagian dukungan dari Hoskinson Center for Formal Mathematics.