Companion Lean untuk Analysis I

 (terrytao.wordpress.com)
2 poin oleh GN⁺ 2025-06-01 | 1 komentar | Bagikan ke WhatsApp
  • Ini adalah proyek yang memindahkan isi inti dari buku analisis real Analysis I karya Terence Tao ke asisten pembuktian Lean
  • Proyek ini memiliki struktur yang sangat selaras dengan tujuan buku aslinya yang menekankan ketelitian, seperti konstruksi sistem bilangan dasar dan logika pembuktian
  • Memanfaatkan pustaka standar Mathlib, tetapi juga mencakup latihan membangun sendiri konsep-konsep utama dan membuktikannya langsung oleh pembaca
  • Pengguna bisa berlatih dengan langsung mengisi bagian kosong (sorry) dalam kode Lean, tanpa solusi resmi, dan dapat memperluasnya melalui fork
  • Berguna bagi pemula Lean maupun pelajar analisis real sebagai kesempatan untuk merasakan penggunaan nyata Mathlib dan Lean

Gambaran umum

  • Proyek open-source yang menyusun ulang buku analisis real "Analysis I" karya Terence Tao dengan alat asisten pembuktian Lean
  • Buku ini lebih berfokus daripada banyak buku analisis lain pada proses konstruksi bilangan asli, bilangan bulat, bilangan rasional, dan bilangan real, beserta alat teori himpunan dan logika yang diperlukan dalam proses tersebut
  • Sebagian besar isi buku berfokus pada pengembangan kemampuan pembuktian yang ketat dan sistematis, sehingga sangat cocok dipadukan dengan asisten pembuktian seperti Lean

Fitur proyek companion Lean

  • Menyediakan "terjemahan" definisi, teorema, dan soal latihan dari buku asli ke dalam format Lean
  • File-file Lean ini memuat banyak bagian kosong (sorry) yang sesuai dengan penyelesaian soal latihan, sehingga pembaca dapat belajar dengan mengisinya sendiri
  • Solusi resmi tidak disediakan, tetapi pembaca dapat mem-fork repositori dan membuat versi jawabannya sendiri

Keterkaitan dengan Mathlib dan perbedaannya

  • Konsep yang sudah diimplementasikan di Mathlib (pustaka matematika standar Lean), seperti bilangan asli, sengaja dibangun ulang secara terpisah, lalu juga disusun proses untuk membuktikan isomorfisme (ekuivalensi) dengan versi Mathlib
  • Sebagai contoh, di Chapter2.Nat, proyek ini membangun definisi bilangan asli versinya sendiri dari nol, terpisah dari bilangan asli Mathlib, menangani hasil-hasil utama secara langsung, lalu pada akhirnya mengajak pengguna berlatih di Lean untuk menunjukkan bahwa kedua versi tersebut setara
  • Mulai bab-bab berikutnya, alurnya semakin banyak memanfaatkan definisi dan fungsi dari Mathlib

Cara belajar dan pemanfaatan

  • Companion Lean ini bukan hanya untuk belajar analisis, tetapi juga berperan sebagai pengantar tentang cara melakukan formalisasi matematika di Lean dan Mathlib
  • Seperti "Natural number game", ada latihan terstruktur yang memungkinkan pengguna mendefinisikan dan melatih objek matematika secara langsung di lingkungan Lean
  • Kodenya sendiri dapat dikompilasi di Lean, tetapi belum diverifikasi sepenuhnya apakah semua soal latihan (sorry) benar-benar bisa diselesaikan; karena itu masih memerlukan playtest dan umpan balik

Open-source dan kontribusi

  • Repositorinya bersifat open-source sehingga siapa pun dapat merujuk, mem-fork, dan berkontribusi
  • Solusi resmi tidak disediakan secara terpisah, dan proyek ini mendukung pembuatan banyak versi solusi
  • Per 31 Mei, proyek ini telah dipindahkan ke repositori independen terpisah

Bacaan terkait

1 komentar

 
GN⁺ 2025-06-01
Opini Hacker News

  • Saya sangat antusias; kalau proyek ini dipindahkan ke repo yang berdiri sendiri, akan lebih mudah dibagikan dan ditemukan orang lain. Saya selalu penasaran dengan matematika, dan Analysis karya Tao adalah buku teks pertama yang benar-benar menunjukkan kepada saya bagaimana matematika dibangun secara ketat dengan cara yang cocok dengan pola pikir pemrograman saya. Setelah itu saya juga jadi tertarik pada Lean, tetapi saya merasa Mathlib agak rumit untuk mempelajari konsep matematika. Karena itu, saya sangat menyukai proyek ini yang berperan sebagai jembatan dari buku ke alat.

    • Saya juga punya pengalaman serupa; saya belajar tentang konvergensi, barisan Cauchy, dan sebagainya, dan saya ingat buku ini diterbitkan oleh penerbit nirlaba India, Hindustan Book Agency, sehingga bisa didapat dengan sangat murah.

  • Bagian paling menarik dari pendidikan matematika dengan Lean menurut saya adalah pemberian umpan balik instan. Jika bukti yang dibuat siswa salah, kodenya tidak akan terkompilasi. Dulu umpan balik harus diberikan langsung oleh manusia seperti TA atau profesor, tetapi sekarang kompiler Lean bisa memberi tahu dengan cepat. Ke depannya saya berharap ada fitur yang bahkan bisa memberi saran perbaikan dengan lebih ramah seperti kompiler Rust (ini mungkin memerlukan LLM khusus).

    • Saya hampir sepenuhnya setuju, tetapi proses memikirkan pembuktian itu sendiri juga penting. Pengalaman matematika saya sudah lama, tetapi ada banyak waktu seperti “surga matematika” ketika saya mengerjakan tugas atau soal di atas kertas sambil berpikir perlahan. Saya khawatir dengan Lean justru orang bisa terdorong ke arah “sekadar gerak tangan”, memasukkan hal secara acak atau mencoba-coba sampai otomatis cocok. Dulu saya juga sempat mencoba coq sebentar, dan yang saya ingat saya hampir terus-menerus hanya mengutak-atik. Kesimpulannya, theorem solver memang berguna dalam banyak hal, tetapi saya khawatir proses mencerna pelan-pelan seperti ini bisa hilang, sehingga jalur menuju internalisasi, konseptualisasi, dan munculnya ide-ide baru ikut melemah. Saya penasaran bagaimana pendapat orang tentang ini.

  • Ada kanal YouTube pribadi tempat kita bisa melihat Terence Tao sendiri menggunakan Lean. Saya bukan ahli di bidang ini, tetapi sekadar menonton bagaimana ia bekerja, baik dengan maupun tanpa LLM, terasa sangat menarik (https://www.youtube.com/@TerenceTao27).

  • Menilai dan membandingkan pendekatan tradisional “gaya buku teks” dengan pendekatan Mathlib akan sangat menarik. Pustaka matematika yang diformalkan umumnya punya kelebihan karena mengekspresikan hasil dengan cara yang segenerik mungkin, dan juga mudah merapikan ulang struktur pembuktiannya agar lebih elegan. Refactoring mudah dilakukan karena sistem selalu melacak ketergantungan logis, sedangkan dengan kertas dan pena itu tidak mudah. Jadi menurut saya wajar untuk bertanya apakah mengajarkan analisis versi “generalisasi maksimal” seperti di Mathlib dalam kuliah universitas itu masuk akal. Menurut saya ini juga pertanyaan yang sama untuk semua bidang matematika berbasis pembuktian lainnya.

    • Setidaknya untuk mata kuliah pengantar, saya rasa itu tidak cocok. Sudah terlalu banyak yang harus masuk ke kurikulum — metode pembuktian, cara pemrograman, dan teori dasar. Pengalaman para profesor yang benar-benar sudah mencobanya juga tampaknya mirip; menurut saya banyak yang menilai itu bagus untuk mahasiswa tingkat lanjut, tetapi membuang waktu untuk mahasiswa pada umumnya.

    • Sebagai matematikawan yang juga sudah lama memrogram, saya rasa formalisasi yang bersifat programatik apa pun tidak akan menumbuhkan pemahaman yang mendasar. Bias saya berasal dari fakta bahwa saya belajar konsep lewat makalah. Kode sering kali sangat tidak peduli pada gaya sehingga keterbacaannya terasa melelahkan; makalah yang sulit dibaca saja sudah berat, dan dalam kode, karena tidak ada standar, menurut pengalaman saya rasanya 10 kali lebih sulit.

  • Menyenangkan melihat theorem proving semakin mendapat perhatian di bidang matematika arus utama seperti analisis. Di PLT, sudah ada contoh terkenal berupa buku Winskel, The Formal Semantics of Programming Languages, yang telah diverifikasi secara formal dengan Isabelle (http://concrete-semantics.org). Jika ingin mulai mencoba theorem proving, saya rasa jalur itu lebih mudah dan layak direkomendasikan. Perlu ditambahkan juga bahwa teorema-teorema dalam analisis pada dasarnya memang cukup sulit.

    • Saya juga tidak akan terkejut kalau pembuktian PL memang punya hambatan masuk yang lebih rendah. Saya juga sering mendengar bahwa rasanya lebih rutin — induksi struktural, menerapkan induksi, membuktikan invariant, mengulang, alurnya seperti itu. Saya memang tidak banyak melakukan theorem proving, tetapi saya belum pernah mencoba membuktikan teorema matematika (terutama analisis) dengan theorem prover. Saya penasaran apakah pembuktian “matematis” menuntut pendekatan yang sangat berbeda, dan seberapa jauh keterampilan di antaranya bisa ditransfer. Sebagai catatan, saya pernah mempelajari Software Foundations in Rocq (mungkin ada port Lean?) dan cukup menikmatinya.

  • Saya rasa proyek dan pendekatan ini sangat cocok untuk topik dasar seperti analisis, tetapi ada dua kekhawatiran.

    1. Hasil-hasil inti analisis di Mathlib ditangani secara terpadu dengan konsep filter, sementara kasus-kasus khusus dibahas terpisah dalam bentuk epsilon-delta. Saya menduga Analysis karya Tao akan memakai pendekatan epsilon-delta yang lebih tradisional.
    2. Mathlib adalah proyek yang berubah cepat, sehingga nama dan strukturnya terus berubah. Informasi keterhubungannya harus dirawat terus-menerus.

  • Menurut saya ini proyek yang sangat keren. Analysis I adalah buku teks matematika “sungguhan” pertama yang sebagai insinyur benar-benar bisa saya pelajari sampai tuntas, dan saya juga punya pengalaman gagal berkali-kali mencoba buku lain (seperti Rudin). Kalau ada versi Lean, saya antusias karena orang yang akrab dengan matematika dan pemrograman sama-sama akan bisa mempelajari konsep dengan lebih ketat.

  • Selama bertahun-tahun sudah ada upaya untuk membuat formalization Lean resmi untuk Analysis I karya Tao, tetapi selalu sulit melaju lebih dari beberapa bab. Selama beberapa waktu saya sendiri juga ingin mencoba ini secara langsung — saya pikir kalau pembuktian formal yang terkait dipublikasikan bersama blog solusi Analysis I (https://taoanalysis.wordpress.com/), itu akan sangat berguna bagi orang yang belajar dari bukunya. Saya sudah pernah membagikan materi yang saya rangkum di Discord privat, tetapi di sini saya bagikan sekaligus tautan-tautan ke proyek Lean referensi yang mungkin berguna bagi banyak orang (github dan gist, dokumen resmi, dll.).

  • Saya penasaran seberapa penting sebenarnya “membuktikan isomorfisme dengan objek yang sesuai di Mathlib”. Mungkin jika bagian isomorfisme itu dihilangkan, secara praktis tidak ada yang berubah? Misalnya, apakah itu benar-benar dipakai untuk hal-hal seperti menerjemahkan teorema secara otomatis?

    • Pembuktian isomorfisme seperti ini

      1. memungkinkan kita membuktikan bahwa objek yang kita buat benar-benar sama dengan objek yang sudah ada di Mathlib, terutama karena di sisi Mathlib objek itu bisa didefinisikan lewat konstruksi yang digeneralisasi secara kompleks, sehingga ini membantu memahami perbedaannya
      2. berperan penting untuk memahami notasi resmi atau istilah yang dipakai saat membaca atau menulis objek tersebut di Mathlib

    • Setidaknya saya rasa ada nilai edukatifnya, dalam arti ini menjadi proses untuk meyakinkan diri sendiri bahwa himpunan dan operasi yang saya konstruksi memang “sama” dengan yang muncul di tempat lain dalam buku.

  • Menyenangkan melihat buku teks berbasis Lean mulai bermunculan. Tapi kenapa tidak ada HoTT (Homotopy Type Theory)? Ada juga artikel yang mengangkat pertanyaan “Should Type Theory (HoTT) replace (ZFC) set theory?” (https://news.ycombinator.com/item?id=43196452). Selain itu, dibagikan juga sumber daya komunitas Lean lain yang muncul di HN minggu ini — “100 theorems in Lean” (https://news.ycombinator.com/item?id=44075061), serta proyek Lean dari DeepMind (https://news.ycombinator.com/item?id=44119725).

    • Tapi saya tidak melihat alasan kenapa harus sampai HoTT. Theorem prover HoTT saat ini masih kurang nyaman digunakan, dokumentasinya juga belum memadai. Saya juga merasa manfaat yang diberikan HoTT belum jelas; biasanya itu hanya terasa berarti saat menangani struktur yang sangat eksotis seperti teori kategori.

    • Karena ini memakai pendekatan buku teks yang sudah ada, jawaban untuk pertanyaan “kenapa bukan HoTT” sebenarnya sudah terkandung di dalamnya. Lagi pula, saya rasa ada banyak ahli yang skeptis terhadap efektivitas pendidikannya.