Matematika dalam Lean

Terjemahan AI Bahasa Indonesia dari Mathematics in Lean, karya Jeremy Avigad dan Patrick Massot. Bab 1–13; contoh, latihan dan solusi Lean. OpenAI Codex gpt-5.6-sol, Ultra; edisi v4.30.0-id.3, 22 Agustus 2026.

Teks: CC BY 4.0. Kode Lean: Apache-2.0. Rujukan istilah: Natanael Karjanto, arXiv:2001.05854. Edisi ini tidak resmi dan tidak ditinjau atau disahkan oleh penulis atau komunitas Lean.

• 1. Pendahuluan
  • 1.1. Memulai
  • 1.2. Ikhtisar
• 2. Dasar-dasar
  • 2.1. Melakukan Perhitungan
  • 2.2. Membuktikan Identitas dalam Struktur Aljabar
  • 2.3. Menggunakan Teorema dan Lema
  • 2.4. Lebih Banyak Contoh Menggunakan apply dan rw
  • 2.5. Membuktikan Fakta tentang Struktur Aljabar
• 3. Logika
  • 3.1. Implikasi dan Kuantor Universal
  • 3.2. Kuantor Eksistensial
  • 3.3. Negasi
  • 3.4. Konjungsi dan Jika-dan-Hanya-Jika
  • 3.5. Disjungsi
  • 3.6. Barisan dan Konvergensi
• 4. Himpunan dan Fungsi
  • 4.1. Himpunan
  • 4.2. Fungsi
  • 4.3. Teorema Schröder–Bernstein
• 5. Teori Bilangan Elementer
  • 5.1. Akar Irasional
  • 5.2. Induksi dan Rekursi
  • 5.3. Bilangan Prima yang Tak Berhingga Banyaknya
  • 5.4. Induksi Lebih Lanjut
• 6. Matematika Diskret
  • 6.1. Finset dan Fintype
  • 6.2. Argumen Pencacahan
  • 6.3. Tipe yang Didefinisikan secara Induktif
• 7. Struktur
  • 7.1. Mendefinisikan Struktur
  • 7.2. Struktur Aljabar
  • 7.3. Membangun Bilangan Bulat Gauss
• 8. Hierarki
  • 8.1. Dasar-Dasar
  • 8.2. Morfisme
  • 8.3. Subobjek
• 9. Grup dan Gelanggang
  • 9.1. Monoid dan Grup
  • 9.2. Gelanggang
• 10. Aljabar Linear
  • 10.1. Ruang vektor dan pemetaan linear
  • 10.2. Subruang dan ruang hasil bagi
  • 10.3. Endomorfisme
  • 10.4. Matriks, basis, dan dimensi
• 11. Topologi
  • 11.1. Filter
  • 11.2. Ruang metrik
  • 11.3. Ruang topologi
• 12. Kalkulus Diferensial
  • 12.1. Kalkulus Diferensial Elementer
  • 12.2. Kalkulus Diferensial pada Ruang Bernorma
• 13. Integrasi dan Teori Ukuran
  • 13.1. Integrasi Elementer
  • 13.2. Teori Ukuran
  • 13.3. Integrasi

Edition history on GitHub · Historical archive