Kompanion Lean untuk Analysis I

 (terrytao.wordpress.com)
2 poin oleh GN⁺ 2025-06-01 | 1 komentar | Bagikan ke WhatsApp
  • Terence Tao memulai sebuah repositori pendamping yang memindahkan definisi, teorema, dan soal latihan dari buku analisis real Analysis I ke dalam kode Lean
  • Karena buku ini secara ketat membahas konstruksi bilangan asli, bilangan bulat, bilangan rasional, bilangan real, serta teori himpunan dan logika, strukturnya sangat cocok untuk dipelajari dengan proof assistant
  • Cakupan saat ini mencakup sebagian Bab 2, teori himpunan dasar 3.1, dan hingga 4.1 bilangan bulat, serta mencakup isomorfisme dengan bilangan asli Mathlib
  • Kodenya dapat dikompilasi di Lean, tetapi masih banyak sorry yang tersisa, dan alih-alih menyediakan jawaban resmi, pendekatan yang disarankan adalah mengisinya di fork repositori
  • Materi ini dapat menjadi jalur alternatif untuk menyelesaikan soal latihan dalam Lean, sekaligus bahan pengantar untuk mempelajari penggunaan Mathlib semakin jauh ke bagian akhir

Proyek memindahkan Analysis I ke Lean

  • Lean companion to “Analysis I” adalah proyek yang “menerjemahkan” berbagai definisi, teorema, dan soal latihan dari Analysis I ke Lean
  • Soal latihan dalam buku juga bisa dikerjakan dengan cara mengisi sorry yang sesuai di kode Lean
  • Jawaban resmi soal latihan tidak direncanakan untuk di-host di kompanyon ini, dan versi yang sudah mengisi sorry dapat dibuat sebagai fork repositori

Mengapa buku ini cocok dengan Lean

  • Analysis I adalah buku yang lebih menekankan isu-isu dasar untuk melengkapi buku analisis real yang sudah ada
    • konstruksi bilangan asli, bilangan bulat, bilangan rasional, dan bilangan real
    • teori himpunan dan logika yang memungkinkan pengembangan pembuktian dengan tingkat ketelitian tinggi
  • Saat buku ini ditulis, proof assistant seperti Coq dan Agda sudah ada, tetapi verifikasi formal bukan fokus saat itu
  • Setelah kemudian mengalami verifikasi formal, menjadi jelas bahwa isi buku ini sangat cocok dengan proof assistant
  • Teori tipe naif yang digunakan secara implisit saat membangun sistem bilangan standar dalam buku ini cocok dengan teori tipe dependen di Lean
  • Dukungan Lean terhadap quotient type juga sejalan dengan cara konstruksi dalam buku

Cakupan yang saat ini sudah dipindahkan ke Lean

Hubungannya dengan Mathlib

  • Formalisasi ini dirancang agar pada beberapa titik terpisah dari pustaka matematika standar Lean, Mathlib, dan pada titik lain bergantung padanya
  • Mathlib sudah memiliki konsep bilangan asli standar
  • Dalam formalisasi Lean ini, mula-mula dikembangkan Chapter2.Nat dengan membangun ulang bilangan asli “secara manual”
    • jika bekerja di namespace Chapter2, ini dapat digunakan sebagai Nat
    • sejumlah hasil dasar yang paralel dengan lemma bantuan tentang bilangan asli di Mathlib disiapkan
    • banyak pembuktian di antaranya dibiarkan sebagai soal latihan pembaca dan saat ini digantikan dengan sorry
  • Pada bagian epilog, dibangun isomorfisme antara bilangan asli alternatif ini dan bilangan asli Mathlib
    • lebih tepatnya, isomorfisme itu sendiri juga dijadikan soal latihan
  • Setelah itu, konstruksi bilangan asli dari Bab 2 tidak lagi dipakai, dan sebagai gantinya digunakan bilangan asli Mathlib
  • Rencananya, semakin ke bab-bab akhir buku, pola ini akan berlanjut dengan ketergantungan yang lebih besar pada definisi dan fungsi Mathlib daripada pada konstruksi internal dari bab-bab awal

Cara penggunaan dan status verifikasi

  • Kode repositori ini dapat dikompilasi di Lean
  • Namun, belum diuji apakah banyak sorry di dalam kode benar-benar semuanya dapat diisi
  • Juga perlu dipastikan apakah lemma bantuan yang diperlukan atau API berkas Lean sudah memadai
    • tujuannya adalah memastikan sorry dapat diisi secara konseptual dan alami tanpa bergantung pada teknik pemrograman Lean yang sulit dipahami
  • Diharapkan ada relawan yang mau playtest kompanyon ini untuk memastikan bahwa soal latihan benar-benar bisa diselesaikan di Lean
  • Umpan balik lain juga sangat diterima

Karakter sebagai bahan pengantar Lean·Mathlib

  • Kompanyon ini dapat digunakan bukan hanya untuk analisis real, tetapi juga sebagai pengantar ke Lean dan Mathlib
  • Dalam hal ini, sifatnya agak mirip dengan Natural number game
  • Natural number game memiliki banyak tumpang tindih tema dengan Bab 2 dari Analysis I

Bacaan terkait

1 komentar

 
GN⁺ 2025-06-01
Pendapat di Hacker News

  • Menurut saya, hal paling menarik saat mengajarkan matematika dengan Lean adalah umpan balik langsung. Jika pembuktian siswa salah, ia tidak akan terkompilasi begitu saja
    Dulu, umpan balik baru bisa didapat jika ada orang seperti asisten dosen, instruktur, atau pakar yang memeriksanya, tetapi sekarang compiler Lean bisa memberi umpan balik dengan cepat
    Ke depannya, akan bagus jika compiler Lean juga bisa memberi umpan balik yang lebih edukatif, seperti compiler Rust yang memberi saran perbaikan kode, dan mungkin diperlukan LLM khusus untuk itu

    • Saya hampir sepenuhnya setuju, tetapi saya khawatir berpikir lambat bisa hilang dari proses belajar pembuktian
      Dulu saat belajar matematika, banyak waktu dihabiskan untuk merenungkan tugas lama-lama sambil mencoba berbagai hal di atas kertas, dan proses itu kadang berujung pada internalisasi konsep serta ide baru
      Dengan Lean, bukankah bisa saja caranya menjadi sekadar mencoba-coba, memeriksa secara acak, lalu menumpahkan banyak percobaan. Saat beberapa kali menyentuh Coq pun, yang saya ingat terutama adalah banyak mengutak-atik dan mencoba ini-itu
    • Acorn sudah bekerja seperti itu. Ketika pembuktian gagal tetapi “hampir benar”, di VS Code ia menampilkan saran seperti berikut
      reduce(r.num, r.denom) = reduce(a, b)
      cross_equals(a, b, r.num, r.denom)
      r.denom * a = r.num * b
      Tidak memakai LLM; ada model lokal kecil yang berjalan di dalam ekstensi VS Code. Semoga suatu hari model lokal kecil itu menjadi cukup kuat hingga jauh melampaui manusia. Detailnya ada di https://acornprover.org/docs/tutorial/proving-a-theorem/.

  • Benar-benar membuat saya antusias. Semoga dipindahkan ke repositori terpisah agar mudah ditemukan dan dikirim ke orang lain
    Saya memang penasaran dengan matematika, dan Analysis karya Tao adalah buku ajar pertama yang menunjukkan bagaimana matematika disusun dengan cara yang ketat seperti yang diharapkan oleh pikiran seorang programmer
    Setelah itu saya juga sedikit mencoba Lean dan merasakan kepuasan serupa, tetapi Mathlib cukup rumit untuk dipakai belajar konsep matematika. Karena itu saya senang ada jembatan antara buku dan alatnya

    • Saya juga belajar hal-hal seperti konvergensi dan barisan Cauchy dari buku itu. Buku tersebut diterbitkan oleh penerbit nirlaba lokal bernama Hindustan Book Agency, jadi harganya juga sangat murah

  • Senang melihat pembuktian teorema mendapatkan momentum pada topik matematika arus utama seperti analisis
    Di bidang teori bahasa pemrograman, ketika alat-alatnya sudah mulai cukup matang pada pertengahan 2010-an, buku ajar representatif seperti The Formal Semantics of Programming Languages karya Winskel pernah diverifikasi secara formal dengan Isabelle. Bukan transkripsi 1:1 yang lengkap, tetapi http://concrete-semantics.org adalah contohnya
    Jika tertarik pada pembuktian teorema, secara pribadi saya melihat bidang itu sebagai titik awal yang jauh lebih mudah. Sebab teorema-teorema analisis sendiri sudah cukup sulit

    • Tidak mengherankan jika pembuktian bahasa pemrograman lebih mudah untuk pemula. Seperti kata orang-orang, tampaknya ada jauh lebih banyak prosedur yang terstruktur
      Melakukan induksi struktural, menerapkan hipotesis induksi untuk menunjukkan bahwa invariant tetap terjaga, lalu terus melanjutkan, semacam itu
      Saya juga belum banyak melakukan pembuktian teorema dan belum pernah melakukan pembuktian “matematis” seperti analisis dengan proof assistant, tetapi saya penasaran seberapa besar transfer keterampilan di antara keduanya jika pembuktian matematika menuntut pendekatan yang jauh berbeda
      Saya juga ingin menyebut Software Foundations dari Rocq. Mungkin ada port Lean-nya, tetapi ketika saya mengikuti bagian awalnya, rasanya cukup nyaman

  • Akan sangat menarik untuk mengevaluasi bagaimana pendekatan arus utama ala “buku ajar” berbeda dari pendekatan Mathlib
    Secara umum, pustaka matematika yang diformalisasi menyatakan hasil seumum mungkin, dan memudahkan refaktorisasi pengembangan pembuktian agar lebih intuitif dan elegan
    Refaktorisasi mudah karena sistem selalu melacak apa yang secara logis mengikuti dari apa. Saat bekerja dengan kertas dan pena, hal itu tidak ada, sehingga peluang untuk pengerjaan ulang sering terlewat
    Pertanyaan yang wajar juga adalah apakah masuk akal mengajarkan analisis real versi “keumuman maksimal” ala Mathlib di tingkat sarjana. Tentu hal yang sama berlaku untuk bidang matematika berbasis pembuktian lainnya

    • Untuk kelas pengantar, saya rasa jelas tidak. Sudah terlalu banyak yang harus dipelajari: cara membuktikan, cara memprogram, dan isi mata kuliah aslinya sendiri
      Setahu saya, pengalaman para dosen yang benar-benar sudah mencobanya juga serupa. Untuk mahasiswa tingkat lanjut mungkin baik-baik saja, tetapi untuk mahasiswa rata-rata, besar kemungkinan hanya akan membuang waktu kelas
    • Sebagai seorang matematikawan yang juga sudah lama memprogram, saya merasa bentuk formalisme ala program apa pun kemungkinan gagal menanamkan pemahaman dasar
      Bias saya memang berasal dari kenyataan bahwa saya mempelajari konsep matematika dari makalah
      Kode memberi beban tambahan yang sangat besar, dan sering kali terasa tidak mengikuti standar gaya apa pun. Sebagai orang yang juga harus membaca makalah matematika yang dinilai tidak bisa dipahami, menurut saya kode 10 kali lebih buruk karena praktis hampir tidak ada standar keterpahaman

  • Di kanal YouTube Terence Tao sendiri juga ada beberapa video tentang menggunakan Lean. https://www.youtube.com/@TerenceTao27
    Saya tidak tahu detailnya, tetapi menarik melihatnya bekerja dengan atau tanpa LLM

  • Untuk topik fundamental seperti analisis, ini proyek yang sangat bagus sekaligus pendekatan yang baik
    Ada dua kekhawatiran yang langsung terlintas. Pertama, hasil-hasil inti analisis di Mathlib menggunakan konsep filter untuk menangani limit secara umum dan terpadu. Meski begitu, sebagian hasil dispesialisasikan dalam bentuk epsilon-delta. Saya rasa Analysis karya Tao akan memakai pendekatan epsilon-delta yang lebih tradisional
    Kedua, Mathlib bergerak cepat dan sering rusak. Nama-nama berubah dan refaktorisasi terus terjadi, sehingga repositori turunan membutuhkan pemeliharaan berkelanjutan

  • Ini pemikiran yang cukup radikal, tapi menurut saya pendidikan matematika seharusnya berfokus pada pembuatan sistem aljabar komputer seperti Mathematica dan pembukti teorema seperti Lean. Visualisasi dan penerapan praktis juga harus sangat disertakan
    Dalam bentuk ekstrem, bisa saja orang sama sekali tidak melakukan matematika di atas kertas, tetapi tetap bisa membuktikan semua yang dipelajari di dalam Lean
    Sistem saat ini berfokus pada perhitungan manual tanpa akhir; rasanya sangat tidak berguna dan membosankan sehingga membuat orang membenci matematika

  • Materi ajar Lean, bagus. Tapi mengapa tidak ada HoTT?
    “Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math?”
    https://news.ycombinator.com/item?id=43196452
    Materi Lean tambahan yang muncul di HN minggu ini:
    “100 theorems in Lean”
    https://news.ycombinator.com/item?id=44075061
    “Google-DeepMind/formal-conjectures: collection of formalized conjectures in lean” https://news.ycombinator.com/item?id=44119725

    • Formalisasi berbagai ide HoTT saat ini sedang dilakukan di komunitas Agda. https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Notes/
      Motivasi persisnya di luar bidang saya, jadi saya tidak tahu, tetapi tampaknya Agda adalah cara yang lebih baik daripada Lean untuk memformalkan ide-ide itu
      Menjelang akhir tahun ini juga akan terbit buku ajar baru yang merupakan pembaruan yang lebih modern dari buku HoTT yang ada, dan ada juga formalisasi Agda
      https://www.cambridge.org/core/books/introduction-to-homotopy-type-theory/0DD31EC06C80797A50ACE807251E80B6
      https://github.com/HoTT-Intro/Agda
    • HoTT adalah topik yang sangat teknis dan sangat sempit, jadi tidak masuk akal menangani dua proyek ambisius seperti ini sekaligus
      HoTT sama sekali belum dekat untuk diterima sebagai standar yang masuk akal, dan bagi kebanyakan orang ini adalah topik yang sudah membuat buntu sejak awal
      Ini mirip seperti bertanya kepada pengembang framework JavaScript mengapa ia tidak membuat framework untuk Elm atau Haskell
    • Saya juga tidak tahu mengapa HoTT harus ada
      Jauh lebih sedikit pekerjaan yang dicurahkan untuk membuat pembukti teorema HoTT mudah digunakan, dan dokumentasinya juga jauh lebih buruk
      Manfaat HoTT juga tidak jelas. Tampaknya hanya mengurangi pekerjaan ketika menangani konstruksi yang sangat esoteris dalam teori kategori
    • Pertanyaan “mengapa tidak ada HoTT” agak aneh
      Terrence Tao punya beberapa buku ajar analisis, dan ini adalah materi pendamping Lean untuk buku pertamanya. Ia tidak punya buku ajar teori tipe, jadi tidak ada teori tipe tingkat tinggi. Dari awal, hal yang ingin dilakukan sama sekali berbeda
    • Fakta bahwa ini adalah materi pendamping untuk buku ajar yang sudah ada saja sudah menjawab “mengapa bukan HoTT”. Alasan lain mungkin karena orang meragukan nilai edukatifnya

  • Sangat keren. Analysis I adalah buku ajar matematika “sungguhan” pertama yang, setelah beberapa kali mencoba buku lain seperti Rudin, saya—seorang insinyur, bukan matematikawan—merasa bisa benar-benar mengikuti dan menyelesaikannya
    Semoga materi pendamping Lean ini membuatnya lebih mudah diakses oleh orang-orang yang akrab dengan matematika dan pemrograman serta ingin belajar secara ketat

  • Selama beberapa tahun terakhir, ada upaya yang terus berlanjut untuk memformalkan buku Analysis I karya Tao dengan Lean, dan ada orang-orang yang mencoba melakukan persis hal yang sedang dilakukan Tao sekarang. Sayangnya, sebagian besar tidak berhasil melampaui beberapa bab awal, dan semoga Tao bisa melangkah lebih jauh
    Saya juga sempat berpikir untuk mencobanya sendiri. Sebab, jika bukti formal untuk tiap soal latihan ditambahkan ke blog penjelasan Analysis I saya, https://taoanalysis.wordpress.com/, itu sepertinya akan berguna bagi orang-orang yang mengikuti buku tersebut
    Saya juga sudah mempostingnya di server Discord privat untuk buku ini, tetapi karena tampaknya bisa membantu di sini juga, saya membagikan materi terkait
    https://github.com/cruhland/lean4-analysis — diambil dari https://github.com/cruhland/lean4-axiomatic
    https://github.com/Shaunticlair/tao-analysis-lean-practice
    https://github.com/vltanh/lean4-analysis-tao
    https://github.com/gabriel128/analysis_in_lean
    https://github.com/mk12/analysis-i
    https://github.com/melembroucarlitos/Tao_Analysis-LEAN
    https://github.com/leanprover-community/NNG4/ — tidak mengikuti buku Tao, tetapi ini adalah versi Lean4 dari Natural Number Game, jadi isinya sangat mirip dengan Bab 2
    https://github.com/djvelleman/STG4/ — ini adalah permainan teori himpunan Lean4, jadi mungkin mirip dengan Bab 3. Namun, di https://github.com/djvelleman/STG4/blob/main/Game/Metadata.lean terlihat import Mathlib.Data.Set.Basic, jadi tampaknya ia mengimpor himpunan Lean alih-alih mendefinisikan himpunan dari awal dan menetapkan aksiomanya. Pendekatan ini bisa membuat Lean tahu “terlalu banyak” tentang teori himpunan, sehingga mungkin kurang cocok untuk tujuan tersebut
    https://gist.github.com/kbuzzard/35bf66993e99cbcd8c9edc4914c9e7fc — untuk konstruksi bilangan bulat
    https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/IntegerGame.lean — mungkin file yang sama seperti di atas
    https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/RationalGameAlgebra.lean — untuk konstruksi bilangan rasional
    https://lean-lang.org/theorem_proving_in_lean4/axioms_and_computation.html#function-extensionality — menunjukkan salah satu cara untuk mendefinisikan tipe Set buatan pengguna