- Sejarah formalisasi matematika tidak dimulai dari Lean; sejak hampir 60 tahun lalu, berbagai garis keturunan sistem sudah mengumpulkan teknik inti dan capaian penting
- Alat seperti AUTOMATH pada 1968, keluarga LCF, HOL, Rocq, ACL2, dan Mizar telah menghasilkan formalisasi luas, dari analisis real hingga teorema bilangan prima, teorema empat warna, dan dugaan Kepler
- Lean membangun definisi matematika modern dengan cepat berkat pustaka besar dan komunitas yang aktif, tetapi propositions as types maupun dependent types bukan satu-satunya jalan bagi proof assistant
- Isabelle menonjolkan otomatisasi yang kuat, keterbacaan tinggi, dan penghindaran dependent types, sambil meneruskan tradisi LCF yang menyusun pemeriksaan bukti lewat abstraction barrier pada kernel tanpa proof object
- Dengan bertambahnya arus kerja ketika AI merapikan bukti terstruktur dan menerjemahkannya ke sistem lain, beban untuk memandang satu alat sebagai standar mutlak ke depan bisa makin berkurang
Sistem awal dan garis keturunan lain
-
AUTOMATH
- AUTOMATH pada 1968 sudah memuat hampir semua elemen yang dibutuhkan untuk formalisasi matematika
- Pada 1977, Jutting memformalkan Foundations of Analysis karya Landau dengan AUTOMATH, dimulai dari logika murni hingga mencapai konstruksi bilangan kompleks
- Ia menggunakan kelas ekuivalensi dan himpunan bilangan rasional, serta membuktikan secara formal kelengkapan Dedekind dari garis bilangan real
- Capaian ini tidak muncul lagi selama 20 tahun, dan baru pada pertengahan 1990-an formalisasi bilangan real kembali dilakukan dalam HOL Light oleh John Harrison dan Isabelle/HOL oleh Jacques Fleuriot
- Notasinya sangat tidak nyaman dan sama sekali tanpa otomatisasi, sehingga buktinya panjang dan sulit dibaca
- Meski begitu, untuk menangani kelas ekuivalensi sistem ini dinilai lebih baik daripada Rocq; tidak seperti setoid hell yang dialami pengguna Rocq, Jutting melakukan formalisasi kelas ekuivalensi dengan tenang
-
Boyer dan Moore
Arus setelah LCF
- Edinburgh LCF berfokus pada teori bahasa pemrograman, tetapi gagasan menempatkan bahasa fungsional sebagai metalanguage untuk proof assistant menyebar luas
- Berbagai kelompok di Cambridge, INRIA, Cornell, dan tempat lain memakai ML untuk membuat alat seperti HOL awal, Coq (kini Rocq), dan Nuprl
- Kelompok HOL berfokus pada verifikasi perangkat keras, tetapi verifikasi perangkat keras floating-point membuat analisis real menjadi perlu
- John Harrison membuktikan hasil matematika serius seperti teorema bilangan prima dalam keluarga HOL melalui rumus integral Cauchy
- Dengan sasaran memverifikasi sebanyak mungkin 100 theorems, HOL Light sering berada di jajaran teratas
- Hingga 2014, sistem-sistem dalam keluarga ini telah memformalkan berbagai teorema tingkat lanjut
- Teorema-teorema ini umumnya memiliki bukti yang panjang dan kompleks, pekerjaan formalisasinya juga sangat besar, dan berperan penting dalam mengurangi keraguan yang masih tersisa pada teorema tersebut
Kebangkitan komunitas Lean
- Para matematikawan menilai capaian formalisasi sebelumnya belum menyentuh konstruksi rumit matematika modern arus utama seperti Grothendieck schemes atau perfectoid spaces
- Tom Hales memilih arah membangun definisi-definisi tersebut sebagai pustaka, memilih Lean dengan fokus pada akumulasi definisi daripada bukti
- Ia mempresentasikan arah ini dalam program Big Proof, dan gagasan serupa juga ikut dibahas
- Kevin Buzzard mendengarnya lalu memutuskan mencoba Lean untuk pendidikan, dan sejak itu penyebarannya makin cepat
- Sebagai titik balik penting komunitas Lean, ditunjukkan bahwa ia keluar dari obsesi pada bukti konstruktif yang lama mendominasi Rocq
- Intuitionism muncul setelah paradoks Russell dan memiliki implikasi tertentu juga bagi konsep bilangan real
- Martin-Löf type theory jelas merupakan formalisme intuitionistik, tetapi Rocq disebut tidak bisa dipandang sesederhana itu
- Meski demikian, dalam makalah-makalah terkait Rocq, bukti konstruktif terus berulang bahkan di tempat-tempat yang tidak relevan atau tidak bermakna, dan kecenderungan ini dianggap menghambat penerapan Rocq pada matematika hingga memberi ruang kepada Lean
propositions as types dan perbedaan dengan LCF
- Propositions as types adalah dualitas yang menghubungkan simbol logika ∀, ∃, →, ∧, ∨ dengan pembentuk tipe Π, Σ, →, ×, +
- Kerangka ini indah dan produktif secara teoretis, tetapi bukan satu-satunya jalan
- Jika proof assistant dibatasi sebagai perangkat lunak yang memeriksa bukti menurut prinsip propositions as types, maka sebagian besar penelitian setengah abad terakhir terdorong keluar dari definisi itu
- Dalam kerangka tersebut, yang tersisa hanya Rocq, Lean, dan Agda
- Bahkan AUTOMATH bukan contoh propositions as types; walau ada unsur mirip Π dan →, logikanya ditetapkan sebagai aksioma seperti dalam buku teks logika umum
- de Bruijn sudah melihat 50 tahun lalu bahwa pemisahan antara tipe dan proposisi itu perlu
- Contoh khasnya, pembagian harus menerima tiga argumen, dan nilai dari (x/y) akan bergantung pada bukti bahwa (y \ne 0), sehingga diperlukan proof irrelevance
- Anggapan bahwa pendekatan LCF sama dengan propositions as types juga ditegaskan sebagai tidak benar
- Rocq dan Lean memiliki Prop sebagai sort untuk proposisi; di sini semua objek bukti dari proposisi yang sama dievaluasi sebagai nilai yang sama dan dengan demikian memberi proof irrelevance
- Namun itu tidak berarti proof object yang sangat besar menghilang; dalam sistem nyata ia tetap ada
- Penemuan inti Robin Milner adalah bahwa dalam LCF proof object itu sendiri tidak diperlukan
- Jika kernel bukti ditempatkan di dalam abstract data type ML, dan aturan inferensi dijadikan konstruktor, maka bukti dapat diperiksa secara dinamis
- Berkat abstraction barrier dari ML, kecurangan dianggap mustahil
- Bahwa term raksasa yang tidak menunjukkan apa pun tetap memakan puluhan MB terasa sangat tidak rasional, terutama di era RAMmageddon
- Kritik juga diarahkan pada penelitian yang masih berlanjut untuk membuat term-term tak perlu itu terlihat lebih elegan
Alasan memilih Isabelle
- Jika rekan-rekan memakai Lean, keahlian tim juga ada di Lean, dan pustaka prasyarat yang dibutuhkan juga ada di Lean, maka memakai Lean adalah pilihan yang wajar
- Namun jika bisa memilih dengan bebas, ada alasan jelas untuk mempertimbangkan Isabelle
-
Otomatisasi
- Otomatisasi terkuat disebut sebagai keunggulannya, dan dibandingkan “hammer” sehari-hari sekalipun, dinilai tidak ada yang menandingi sledgehammer
- Disebut juga bahwa ranah aljabar komputasional perlu dibahas tersendiri
-
Keterbacaan
-
Menghindari dependent types
- Karena tidak memiliki dependent types, Isabelle menghindari universe level dan berbagai keanehan yang menyulitkan pemula
- Bahkan dalam mathlib milik Lean maupun SSReflect dan Mathematical Components milik Rocq, penggunaan dependent types disebut tidak dianjurkan
- Kesulitan inti dependent types adalah bahwa jika diterapkan sepenuhnya, type checking itu sendiri menjadi tak dapat diputuskan
- Hal ini karena penentuan kesetaraan juga tak dapat diputuskan, dan pada awalnya keadaan ini dianggap wajar
- Sejak sekitar 1990, konsensus bergeser ke arah membuat type checking dapat diputuskan dengan menurunkan kesetaraan menjadi definitional/intensional equality
- Akibatnya, (T(N+1)) dan (T(1+N)) menjadi tipe yang berbeda
- Batasan seperti ini juga memengaruhi bukti nyata, dan pemeriksaan definitional equality sendiri tetap mahal secara komputasi
Matematika modern tanpa dependent types pun memungkinkan
- Per 2017, ditulis bahwa penilaian tentang sejauh mana matematika dapat ditangani Isabelle jauh lebih berhati-hati
- Saat itu, topik-topik seperti berikut mudah tampak seolah benar-benar membutuhkan dependent types
- Namun melalui riset terkait Alexandria, banyak hal dipelajari, dan kesimpulannya adalah bahwa yang penting ialah tidak memaksa semuanya masuk ke dalam tipe
Arah ke depan dan AI
- Lean melakukan banyak hal dengan benar, dan bahkan mendukung blok bukti bertingkat, sehingga berpotensi menjadi bahasa bukti yang cukup mudah dibaca
- Kini komunitas Lean perlu benar-benar memanfaatkan fitur semacam itu, sementara pengguna Isabelle disebut pada umumnya sudah melakukannya
- Daripada proof object yang bisa diperiksa komputer, yang lebih penting adalah kejernihan teks bukti yang sungguh bisa dibaca manusia
- Kebangkitan AI membuat perbedaan ini makin jelas
- Bukti yang dibuat AI sering berantakan, tetapi mudah dirapikan dengan sledgehammer, dan jika strukturnya baik maka detail yang berlebihan pun masih bisa dibaca
- Dengan begitu, alur pengerjaan lebih mudah dipahami dan disederhanakan ke bentuk yang lebih ringkas
- Belakangan bahkan muncul riset tentang model bahasa yang langsung memanggil sledgehammer
- AI juga dapat dengan mudah menerjemahkan bukti terstruktur yang mudah dibaca dari satu proof assistant ke proof assistant lain
- Jika demikian, beban dalam memilih sistem mana yang akan dipakai pun berkurang
Melengkapi kekurangan tentang Mizar
- Sejarah formalisasi matematika tidak bisa lengkap tanpa Mizar dan pustaka matematika yang sangat besar miliknya
- Bahasa Isar pada Isabelle juga banyak dipengaruhi oleh Mizar
- Disebutkan pula koreksi terpisah atas kelalaian ini, dan bahwa tulisan berikutnya akan membahas Mizar
1 komentar
Pendapat Hacker News
Kebanyakan pembaca HN lebih dekat ke programmer daripada matematikawan, jadi melihat Lean dari sudut pandang pemrograman terasa lebih praktis daripada dari sisi pembuktian matematika
Sebagai buku yang membahas Lean dari perspektif pemrograman fungsional, https://leanprover.github.io/functional_programming_in_lean/ cukup bagus
Saya juga sedang belajar Lean jadi mungkin masih punya pandangan terlalu optimistis sebagai pemula, tetapi tujuan saya adalah menulis dan membuktikan kode programmer biasa seperti algoritme kompresi/dekompresi nyata, seperti contoh lean-zip belakangan ini
https://github.com/kiranandcode/lean-zip/blob/master/Zip/Nat...
https://github.com/dharmatech/symbolism.lean
Ini port dari kode C#, dan daya ekspresif Lean luar biasa besar
Saya pernah melihatnya sempat cukup ramai dibicarakan, tapi belakangan tidak terlalu mengikuti bidang ini secara detail
Lalu saya melihat dua hambatan lagi. Pertama, mengetahui apa yang harus dilakukan perangkat lunak itu sendiri sudah sulit, dan apa yang ingin dilakukan pengguna belum tentu sama dengan hal yang dibayar pelanggan
Kedua, kualitas kerja banyak pengembang begitu rendah sehingga sulit berharap mereka akan lebih mahir menangani bahasa kebenaran daripada bahasa seperti Java
Namun yang kedua ini bisa saja hilang jika digantikan sistem AI yang memberi perhatian yang diperlukan, dan kalau itu terjadi situasinya mungkin berubah
Menurut saya, seperti halnya matematika yang sudah ditinggalkan pemrograman fungsional, itu juga tidak terlalu relevan bagi kebanyakan programmer
Penulis tampaknya cukup salah paham soal Lean, dan itu justru lebih mengejutkan karena ia terlihat seperti orang yang paham bidang ini
Ia tampaknya menganggap Lean mempertahankan objek bukti apa adanya lalu pada akhirnya memeriksa satu objek bukti raksasa dengan semua definisi di-expand, padahal kenyataannya jauh dari itu
Lean pada dasarnya mengimplementasikan optimisasi yang dipuji penulis sebagai kelebihan LCF dengan cara yang hampir sama. Analogi kasarnya, seperti menghapus papan tulis sambil melanjutkan pembuktian
Di Lean4, jika ditulis dengan
theoremalih-alihdef, objek buktinya tidak dipakai lagi, dan ini bukan sekadar optimisasi, melainkan sifat inti bahasa. theorem bersifat opaqueKalaupun term bukti masih tersisa, itu hanya agar pengguna bisa melihatnya dalam mode interaktif, dan kernel bahkan tidak bisa peduli apa isi objek bukti itu
Dalam LCF, bukti dan term itu berbeda, dan menurut saya memang seharusnya begitu. Kebingungan ala Curry-Howard seperti ini tidak perlu, tetapi banyak orang mengira itulah satu-satunya cara melakukan matematika dengan komputer
Kalau mau, di LCF pun bukti bisa disimpan dan dimanfaatkan, dan di Lean pun kalau mau bisa dihilangkan lewat optimisasi
Pendekatan tipe abstrak mungkin menghemat memori sedikit, tetapi hanya beda faktor konstan dan bukan perbaikan asimtotik
Keluhan bahwa Lean membuang-buang puluhan MB mungkin penting pada 1980-an atau 1990-an, tetapi sekarang sepertinya bukan lagi keunggulan yang begitu menentukan
Saya sering mendengar Lean bagus untuk pemrograman fungsional, tetapi kalau datang dari Agda rasanya seperti downgrade yang cukup kikuk
Tactic-nya juga dibilang bagus, tetapi dalam pengalaman saya tactic Coq lebih kuat dan lebih nyaman dipakai
Mungkin ini semua cuma bias kesan pertama, tetapi sejauh ini kekuatan Lean tampaknya bukan karena ia paling unggul dalam satu hal, melainkan karena secara keseluruhan cukup baik dan komunitasnya besar
Saya paham kenapa itu menarik, tetapi sayang juga rasanya karena ada sedikit keindahan dan kekuatan yang hilang sebagai gantinya
Namun efek seperti ini sering tampak abadi pada saat itu, padahal kenyataannya tidak selama yang dibayangkan. Kalau memang hanya itu yang penting, Perl seharusnya masih tetap raksasa sampai sekarang
Di Lean, yang terutama besar pengaruhnya adalah mereka lebih dulu punya library besar. Mirip seperti peran CPAN bagi Perl
Tetapi kalau melihat hukum penskalaan, bagi kebanyakan pengguna nilai library besar kemungkinan hanya bertambah kira-kira sebesar log dari ukurannya
https://pdodds.w3.uvm.edu/teaching/courses/2009-08UVM-300/do...
Di awal jurang ini tampak mustahil dikejar, tetapi tanpa harus mengejar skala yang sama pun, pada titik tertentu kemudahan pakai menjadi lebih penting
Selain itu, porting library matematika juga cocok untuk LLM. Sumbernya sudah terverifikasi, targetnya juga bisa diverifikasi, dan jalur penalarannya umumnya bisa dipindahkan
Sebaliknya, ini berarti berkat LLM hambatan bekerja di platform kecil juga lebih rendah dari perkiraan. Jika saya bisa memindahkan library mereka ke platform saya, besar kemungkinan pembuktian saya juga bisa dipindahkan ke sana
Alat yang sempurna bukan inti persoalannya; yang lebih penting adalah menyelesaikan pekerjaan dengan alat yang cukup bagus
Lean tampaknya punya ruang untuk berkembang sebagai bahasa fungsional untuk pengembangan perangkat lunak, sampai-sampai benar-benar bisa menjadi penerus Haskell
Perbedaannya terutama terasa pada dukungan tooling. Dokumentasi Agda kurang bagus, memasangnya dan menjalankannya di sistem juga merepotkan, dan secara praktis sangat mendorong penggunaan Emacs
Sebaliknya, Lean bahkan punya panduan menulis utilitas
catdalam dokumentasi resminya, dan secara umum memberi pengalaman tooling yang jauh lebih modernBiasanya pujian banyak saya dengar pada dependent pattern matching, dan di bagian itu Lean memang terasa cukup lemah
Tetapi kalau dalam FP umum pun Agda terasa lebih ramah, saya ingin tahu di aspek mana
Isabelle/HOL bahasanya sendiri lumayan, tetapi tooling-nya punya cacat mendalam bahkan di luar pendekatan yang berpusat pada desktop
Bahasanya tidak benar-benar lebih baik dari Lean, hanya berbeda, dan saya setuju dengan beberapa kritik terhadap tipe dependen
Pada akhirnya kedua bahasa itu membuat trade-off yang berbeda, dan pilihan itu tampaknya membuat masing-masing menjadi alat yang cukup efisien di wilayahnya. Ranah pembuktian sendiri begitu luas sehingga tiap paradigma punya kekuatan dan kelemahannya, dan Lean hanya terspesialisasi di bagian yang berbeda
Sledgehammer bagus, tetapi rasanya tinggal soal waktu sampai Lean punya sesuatu yang serupa
Pada tahap eksplorasi itu bisa berguna, tetapi boros sumber daya, dan meski bisa membuat bukti lebih singkat, untuk kode yang dipublikasikan saya lebih suka seluruh langkah bukti terlihat jelas daripada
by sledgehammeryang setengah terasa seperti sihirSebaliknya, mengembangkan Isabelle sendiri jauh lebih menyakitkan daripada Lean, terutama dalam berkomunikasi dengan para pengembangnya
Sikap di mailing list seperti tidak ada bug, yang ada hanya perilaku tak terduga terlihat kekanak-kanakan dan tidak profesional
Dan mengejek penggunaan RAM sistem mirip Lean juga cukup lucu kalau melihat rakus memorinya Isabelle sendiri
Praktis tingkat kesulitannya hampir sama dengan menggunakan bukti formal itu sendiri
Mungkin saya tertukar dengan HOL lain
grinddi Mathlibhttps://leanprover-community.github.io/mathlib4_docs/Init/Gr...
Hal menarik dari Lean adalah Lean itu bahasa, tetapi yang paling sering dibicarakan orang sebenarnya adalah library bernama Mathlib
Para pembuat Mathlib tampak cukup pragmatis, sehingga mereka memasukkan logika klasik ke dalam tipe Lean dan hanya memakai sebagian logika intuisionistik
“Sesuatu tidak bisa sekaligus benar dan salah” bukanlah hukum tertium non datur, melainkan hukum nonkontradiksi
Hukum tertium non datur berarti
pbenar ataunot pbenarhttps://en.wikipedia.org/wiki/Law_of_noncontradiction
https://www.cslib.io https://www.github.com/leanprover/cslib
Logika intuisionistik pada dasarnya bermakna sebagai upaya mengubah argumen matematika menjadi konstruksi yang dapat dihitung, jadi menarik melihat bagaimana mereka akan menangani persoalan ini
Sebenarnya begitu menulis algoritme di Lean, kita sudah masuk ke semacam batasan konstruktif dalam bentuk apa pun, dan untuk tujuan itu mungkin tingkat logika seperti itu sudah cukup
penyangkalan, kemarahan, tawar-menawar, depresi, penerimaan
Kuliah dan tulisan terkait dari Andrej Bauer juga layak dilihat
https://www.youtube.com/watch?v=21qPOReu4FI
http://dx.doi.org/10.1090/bull/1556
Menurut saya tulisan seperti ini perlu lebih banyak
Terhadap pola pikir kelompok yang seolah semuanya sudah jelas dan tinggal mendorong pokoknya pakai X, selalu ada alasan yang cukup meyakinkan untuk setidaknya meninjau alternatif
Walaupun akhirnya tetap meninggalkan alternatif dan memilih arus utama, menurut saya lebih baik memilih sambil memahami medannya
Bahkan sekarang kita sudah membuat terlalu banyak framework dan alternatif, mungkin juga karena itu menyenangkan
Alih-alih memperbaiki alat yang ada atau sekadar menyelesaikan pekerjaan nyata, kita sering terus menambah bahasa, library, dan build tool tanpa henti
Menurut saya justru akan lebih baik jika jumlah bahasa, library, dan build tool sekarang hanya setengahnya
Semakin jauh dari arus utama, dokumentasi makin sedikit, bug makin banyak karena sudut yang kurang dijelajahi, dan orang yang bisa dimintai bantuan makin sedikit
Kalau pilihan sudah menumpuk lebih dari dua puluh, secara rata-rata memang lebih masuk akal memilih opsi standar lalu lanjut. Perhatian itu terbatas; kalau harus menulis laporan investigasi untuk tiap dependensi, masalah inti justru tidak terselesaikan
Ada dua pengecualian, yaitu ketika alat standar benar-benar tidak cocok dengan use case saya, atau ketika alat standar itu sendiri sangat tumpang tindih dengan masalah inti yang ingin saya pecahkan
Diskusi seperti ini terasa mirip dengan tulisan-tulisan yang menyoroti keterbatasan Python untuk komputasi ilmiah
Begitu sebuah komunitas berkumpul melewati massa kritis di sekitar alat yang lumayan baik, itu mengalahkan hampir semua faktor lain
Momentum muncul, tutorial, tulisan penjelas, dan dokumentasi yang lebih baik menumpuk, hingga praktis mencapai escape velocity
Lean tampaknya tepat berada di posisi itu sekarang, apalagi dengan pendukung kuat seperti Terrance Tao
Jadi, pernyataan bahwa “bahasa X lebih baik” tidak sepenuhnya salah, tetapi mudah meleset dari pertanyaan yang sebenarnya penting
Kuncinya adalah apakah itu benar-benar lebih baik daripada alat yang semua orang sudah kenal, bisa langsung dipakai, dan terus menerima lebih banyak waktu untuk perbaikan
Pada akhirnya ini terlihat seperti situasi worse is better, atau bahwa bagus dan populer saja sudah cukup
Terutama karena di bidang ini hasil terjemahannya bisa diverifikasi otomatis sampai tingkat yang cukup tinggi, sehingga pilihan platform itu sendiri mungkin bukan masalah besar
AI bisa menulis kode sendiri meski tidak ada library komunitas raksasa, dan bisa membaca dokumentasi serta spesifikasi langsung tanpa perlu sejuta tutorial beredar di internet
Tidak perlu menghindari bahasa yang tak punya pasar kerja. AI tidak sedang membangun karier; ia hanya perlu mengerjakan tugas yang ada saat itu
Karena itu, bahasa kecil dan DSL yang dulu hampir tidak punya peluang kini lebih mungkin diadopsi
Monokultur bahasa yang bertahan lama dalam pemrograman pun bisa saja diakhiri oleh AI
Pernyataan bahwa “hampir semua yang diformalisasikan dengan sistem apa pun hari ini mungkin juga bisa diformalisasikan di AUTOMATH” mirip dengan mengatakan bahwa apa pun yang ditulis dengan bahasa modern saat ini juga bisa ditulis dengan assembly 50 tahun lalu
Secara teknis benar, tetapi secara ekonomi sama sekali berbeda
Sekitar 15 tahun lalu saya sempat mencoba Coq/Rocq dan beberapa alat lain, dan yang sulit dipahami bukan hanya konsepnya, tetapi perangkat lunaknya sendiri
Hal aneh pada proof assistant / interactive theorem prover adalah bahwa karena sifatnya interaktif, bentuknya menjadi gabungan bahasa dan IDE, dan dalam praktiknya keduanya terikat kuat
Karena itu sulit membicarakan bahasanya secara terpisah; kita juga harus melihat lingkungan tempat ia dipakai
Saya juga bukan penggemar berat VS Code, tetapi jelas bahwa IDE yang dapat diperluas dan dipakai begitu banyak orang, dengan investasi besar dan pemolesan yang matang, jauh lebih unggul daripada lingkungan alternatif
Jalur masuk yang bagus seperti Natural Numbers Game tampaknya juga dimungkinkan oleh kemampuan VS Code untuk di-hack dan oleh ekosistemnya
Namun saat belajar Lean, yang saya khawatirkan adalah ekstensibilitas sintaks sebagai pedang bermata dua
Setelah mempelajari sebuah bahasa, orang ingin bisa membaca kode yang ditulis dengannya, tetapi kalau tiap proyek mulai membuat DSL-nya sendiri dalam jumlah besar, itu bisa tak terkendali
Pada akhirnya ini bergantung pada seberapa menahan diri komunitas dan ekosistemnya, jadi saya melihatnya dengan campuran harap dan khawatir
Lean bukan proof assistant yang paling dicintai matematikawan, dan juga bukan alat yang paling cocok untuk verifikasi formal perangkat lunak
Tetapi ia lumayan mampu melakukan keduanya, dan sebagai gantinya berhasil menangkap momentum yang paling sulit didapat
Ditambah lagi, di era AI jumlah kode buatan manusia yang tersedia secara publik langsung memengaruhi seberapa baik agen dapat menghasilkan kode baru, sehingga momentum itu menjadi makin kuat