Matematika itu berhantu

• Lean adalah bahasa pemrograman yang dirancang untuk memformalkan matematika, sehingga memungkinkan matematikawan memperlakukan teorema matematika seperti kode
• Pengguna menulis teorema, bukti, aksioma dalam bentuk kode, dan proses pembuktian dilakukan melalui kumpulan perintah bernama tactic
• Meskipun bukti belum benar-benar diselesaikan, kita dapat menutupnya sementara dengan sorry; ini adalah bukti semu yang mirip dengan any di TypeScript
• Jika menambahkan aksioma yang salah (misalnya 2 = 3), maka muncul risiko kontradiksi logis dan kemungkinan membuktikan setiap klaim
• Karena Lean hanya menghasilkan kesimpulan atas dasar aksioma yang dipilih dan sistem pembuktian yang logis, menjaga validitas matematika menjadi sangat penting

---

Lean: Matematika seperti kode

• Lean adalah bahasa pemrograman yang dibuat khusus untuk menulis matematika yang terformal
• Melalui Lean, para matematikawan dapat mengekspresikan matematika dalam bentuk kode dan mengatur teorema serta bukti mereka agar dapat berkolaborasi dan berbagi
• Ini menggambarkan masa depan di mana pengetahuan matematika manusia dalam jumlah besar akan bisa diverifikasi dan dikomposisi secara mekanis dalam bentuk kode

Langkah pertama dalam membuktikan dengan Lean

• Bentuk theorem two_eq_two : 2 = 2 := by sorry memungkinkan deklarasi teorema sederhana di Lean
• Saat bukti belum selesai, sorry dapat dimasukkan, tetapi ini hanya solusi sementara, bukan bukti yang sebenarnya
  • sorry lolos pemeriksaan verifikasi bukti Lean, namun tidak dapat dipercaya secara logis
• Untuk bukti yang lengkap, digunakan tactic seperti rfl (reflexivity) untuk membuktikan persamaan yang jelas seperti 2 = 2
• Bagian yang sudah terbukti dapat digunakan kembali di teorema lain menggunakan exact, sehingga menekankan modularitas

Aksioma dan kontradiksi: ketika matematika dianggap berhantu

• Jika menambahkan aksioma seperti axiom math_is_haunted : 2 = 3, Lean akan menganggapnya benar
• Aksioma ini dapat dipakai dalam proses pembuktian berikutnya, hingga memungkinkan pembuktian simpulan yang tidak masuk akal secara matematika, misalnya 2 + 2 = 6
• Dengan tactic rewrite, 2 bisa diganti menjadi 3 dan proses pembuktian persamaan dapat diselesaikan dengan rfl
• Bila kontradiksi dipicu oleh aksioma yang tidak tepat, di Lean juga terjadi keadaan setiap proposisi dapat dibuktikan (keruntuhan logis)
• Pada awal abad ke-20, kontradiksi dalam sistem aksioma seperti Paradoks Russell memicu refleksi mendasar dalam matematika
• Dengan demikian, Lean menunjukkan bahwa pemilihan aksioma sangat menentukan dalam menjaga kewajaran sistem logika

Lean sebagai proof checker

• Jika aksioma dipilih dengan tepat dan Lean secara logis benar, maka akan menghasilkan kesimpulan dengan keandalan teoritis
• Dari persamaan sederhana hingga teorema yang sangat kompleks (misalnya Fermat's Last Theorem), semuanya diverifikasi dengan prinsip yang sama
• Teorema besar dibangun sebagai akumulasi bukti berulang dari teorema dan substruktur, sehingga keseluruhan strukturnya terbentuk secara bertingkat
• Sebagai contoh, proyek skala besar untuk memformalkan Fermat's Last Theorem di Lean sedang berjalan, dan akhirnya diharapkan terselesaikan sistem bukti formal tanpa sorry

Kenikmatan mempelajari Lean

• Pembuktian dengan Lean adalah perpaduan kreatif antara pemrograman dan matematika
• Mulai dari cara membuktikan proposisi sederhana, hingga bertahap membangun matematika yang lebih kompleks dan mendalam secara ketat, itulah kenikmatan utamanya
• Materi tutorial resmi dan komunitas (seperti Natural Numbers Game, Mathematics in Lean, dan lainnya) sangat cocok untuk pemula
• Dengan Lean, Anda memformalkan logika secara langsung dan bisa menemukan kembali keindahan ide serta argumen yang cerdik
• Pada akhirnya, artikel menyimpulkan bahwa tanpa alasan apa pun, bagi jenis orang tertentu, Lean menghadirkan kesenangan yang khas

[GN⁺]

Komentar Hacker News

• Belakangan ini saya memikirkan ide untuk menulis ulang berita atau artikel nonfiksi menggunakan sistem seperti Lean (atau Lean itu sendiri), dengan memperlakukan setiap pernyataan sebagai teorema yang harus dibuktikan, dan membiarkan pembuktiannya juga mencakup kutipan; misalnya, bisa diperlakukan sebagai bukti komposit seperti “jika tiga sumber yang saya setujui menyatakan ini sebagai fakta, maka ini adalah fakta”, dan saya pikir mungkin saja menandai seluruh dokumen agar klaim yang “terbukti” bisa ditampilkan menonjol; memang tidak sempurna, tetapi ini semacam upaya memecahkan kembali lewat teknologi ketelitian yang dulu ditanggung media
  • Memformalkan pernyataan bahasa alami adalah bidang yang penuh dengan banyak rintangan, karena alasan yang mirip dengan sulitnya menulis kode yang berinteraksi dengan dunia nyata; semua konsep yang kita anggap biasa saja (identitas, waktu, kausalitas, dan sebagainya) harus ditangani dengan rinci di dalam formalisme agar fakta-fakta bisa saling terhubung atau bahkan bisa diekspresikan; meski begitu, masalah ini benar-benar menarik, OpenCog adalah proyek yang mendorong bidang ini sampai sejauh mungkin, dan ada juga bidang riset tersendiri di akademia yang disebut knowledge representation and reasoning (KRR); jurnal IJCAI juga penuh dengan riset terkait ini, dan para filsuf telah menulis banyak logika untuk memformalkan berbagai jenis argumen seperti waktu/modalitas/probabilitas, tetapi sayangnya ini tidak mudah digabungkan satu sama lain (kecuali mungkin kalau itu sudah dipecahkan baru-baru ini)
  • Saya rasa keyakinan terpenting yang perlu kita miliki terhadap berita kebanyakan bukan sesuatu yang bisa dibuktikan sebagai kumpulan pernyataan absolut; alat yang menghitung rantai penalaran seperti probabilitas Bayesian tampaknya lebih cocok, dan saya pernah melihat alat untuk estimasi numerik semacam ini
  • Setelah mengambil matematika di universitas, kemampuan menulis nonfiksi saya meningkat pesat; saya pernah membaca esai yang ditulis SO saya dan adik perempuan saya, lalu menerapkan ketelitian seperti saat melihat bukti logis, misalnya “di sini kamu bilang C berasal dari B, tetapi alasan B berasal dari A sebenarnya hilang, jadi kamu tidak bisa bilang C berasal dari A”; tampaknya mungkin membuat ini menjadi program dengan alat seperti LLM, tetapi ada batasan yang jelas karena halusinasi (menghasilkan klaim yang tidak ada faktanya)
  • Perlu hati-hati, pendekatan seperti ini pada dasarnya bisa dengan mudah memberi aura objektivitas logis pada klaim yang betapapun radikal atau tidak masuk akalnya; pandangan politik Gottlob Frege, salah satu bapak logika modern, bisa menjadi peringatan tautan terkait
  • Sepertinya akan lebih menarik kalau ada cara memetakan seluruh struktur argumen untuk topik tertentu seperti peta; misalnya dimulai dari pertanyaan besar seperti “Apakah Tuhan ada?”, lalu membentangkan secara hierarkis semua argumen pro dan kontra, sanggahan terhadapnya, dan sanggahan atas sanggahan itu; untuk tiap klaim, kutipan seperti “Plato membuat argumen seperti ini” dipakai bukan sebagai dasar pembenaran melainkan untuk memberi konteks historis; intinya bukan menentukan pemenang, melainkan membuat peta argumen agar kita tidak terus berputar pada poin yang sama
• Jadi, apakah maksudnya kita pada akhirnya sedang membuat semacam kamus pembuktian yang berawal dari beberapa kebenaran yang dianggap aksiomatis, lalu berbagai bukti disusun secara logis di atasnya? Kalau begitu, bukti tambahan hanyalah kombinasi logis dari bukti-bukti yang sudah ada. Saya ingin ini dijadikan game bergaya Zachtronics! Ada game bernama Euclidea yang memberi nuansa seperti ini di bidang geometri, dan konsep membangun menara logika seperti ini terasa sangat menarik. Saya jadi penasaran apakah matematika murni memang seperti ini, apakah profesor matematika murni merasakan kegembiraan saat memperluas kamus logika ini, dan saya juga ingat sepertinya pernah ada matematikawan terkenal yang membuat daftar bukti dasar; kalau ada yang tahu siapa/apa itu dan apa sebutannya, akan bagus. Mungkin itu adalah aksioma (axioms)
  • Sebenarnya sudah ada game terkait, meski mungkin tidak persis seperti yang Anda mau (dan bukan game untuk membangun seluruh matematika); saya sudah mencobanya dan cukup menyenangkan; yang disebut dalam artikel ini, leanprover-community/nng4, adalah contohnya
  • Menanggapi “tolong jadikan ini game bergaya Zachtronics”, matematika itu sendiri bisa dibilang memang game itu (sedikit bercanda), walaupun saya rasa versi game-nya juga akan benar-benar seru; matematika murni memang sistem semacam itu; di masa sarjana rasanya memang seperti itu, lalu ketika naik ke penelitian makalah rasanya agak berbeda; kalau mau sensasi seperti game, saya juga menyarankan mencari buku teks aljabar abstrak seperti Dummit and Foote; ada keseruan bergaya game dalam pembuktian, dan untuk buku-buku terkenal biasanya ada penjelasan daring kalau Anda mentok
  • Mungkin yang Anda maksud adalah aksioma Euclid, yakni sistem tempat konsep seperti titik, garis, bidang, dan garis sejajar didefinisikan; di atas bola alih-alih bidang, sistem ini runtuh; atau mungkin Anda merujuk ke teori himpunan Zermelo-Fraenkel (ZF/ZFC), yang menjadi landasan tempat seluruh matematika modern dibangun
  • Ada juga game bernama Bombe, varian Minesweeper; alih-alih membuka sel secara langsung, Anda bermain dengan membuat aturan seperti “dalam kondisi apa bendera bisa dipasang”; makin tinggi levelnya, aturan-aturan itu saling berantai seperti lemma (teorema bantu), dan ketika kemampuan pemain meningkat, batasan toolset juga bisa dilonggarkan sehingga generalisasi menjadi mungkin tautan game
  • Pada dasarnya matematika adalah proses memulai dari aksioma lalu menurunkan kesimpulan; tentu itu bukan keseluruhannya, tetapi di level saya saat ini saya memahaminya seperti itu
• Sedikit nitpicking, tetapi agak aneh mengatakan teorema two_eq_two terlihat seperti fungsi; karena tidak punya argumen, ia justru lebih mirip konstanta (meskipun tentu saya tahu konstanta juga fungsi tanpa argumen). Menurut saya akan lebih meyakinkan jika memakai x_eq_x di bawah ini lalu menerapkannya seperti fungsi dalam 2_eq_2

  theorem x_eq_x (x:nat) : x = x := by
    rfl
  
  theorem 2_eq_2 : 2 = 2 := by
    exact (x_eq_x 2)
  

  Di sini x_eq_x memang terlihat seperti fungsi, dan dalam 2_eq_2 benar-benar dipakai seperti itu
  • Itu koreksi yang benar! Saya tidak melakukannya begitu karena cara Lean menangani argumen (terutama konsep seperti dependent types — memberi x lalu mengembalikan bukti x = x) sendiri agak asing bagi saya, dan itu topik yang perlu dibahas terpisah; saya berencana membahasnya di artikel berikutnya
• Kesulitan yang saya rasakan saat belajar Lean adalah tactics (rfl dan semacamnya) terlalu menyeluruh, dan bahkan lewat tutorial pun sulit memahami makna tepatnya; misalnya dalam C kita bisa menelusuri perubahan state sampai level bit, tetapi Lean terasa agak kabur; dan sintaks tactic rewrite (rw) juga terasa tidak alami
  • Di Coq (sekarang Rocq) juga selalu sulit membiasakan diri dengan tactics; misalnya saat ada “A = B” dan “P(A,A)”, saya ingin mengubahnya menjadi “P(A,B)”, tetapi ada pengalaman rewrite tidak jalan karena alasan yang sulit dijelaskan (mungkin masalah definisi struktur perantara); sebaliknya, Metamath dan database set.mm membuat kita membuktikan sepenuhnya dengan penalaran konkret tanpa tactic sama sekali (hanya memakai aturan inferensi seperti ax-mp), tetapi itu pun tidak mudah karena Anda harus menghafal banyak utility lemma yang layak pakai
  • Itu salah satu alasan saya lebih menyukai Agda; Agda pada dasarnya hampir tidak punya tactic, dan dengan memanfaatkan Curry-Howard correspondence kita langsung menulis term bukti sebagai bahasa pemrograman fungsional; sebagai gantinya, kalau malas membuat abstraksi dan fungsi, hal-hal sepele pun bisa jadi luar biasa merepotkan, jadi disiplin itu penting
  • Setidaknya di Lean, ada fakta bahwa definisi tactic bisa dibuka dengan “go to definition” untuk melihat cara kerjanya di dalam; saat belajar ini memang terasa berat karena jumlahnya banyak, tetapi pada akhirnya semuanya bisa diperiksa (meski kalau sudah turun ke type theory dasar, intuisi saya mulai goyah); dan Anda bilang sintaks rewrite terasa tidak alami, jadi saya penasaran, seperti apa sintaks rewrite yang terasa alami menurut Anda?
  • Yang menarik adalah semua tactics berada di luar kernel bukti, sebagai kode “level pengguna”; ini masuk akal karena kita ingin menjaga kernel kecil yang sudah tervalidasi tetap tidak berubah, tetapi ini juga berarti bukti lama bisa rusak saat tactics diperbarui atau diubah; saya penasaran sejauh mana ini benar-benar jadi masalah dalam praktik
  • Berbeda dari dugaan saya, di Lean reflection dan rewrite tampaknya justru lebih mendasar daripada addition; Lean menyediakan addition secara bawaan, tetapi kita sepertinya harus selalu menulis rfl atau rewrite; mungkin Lean punya semacam prelude yang mengotomatiskan ini
• Saya penasaran apakah ada cara membaca proof di Lean secara noninteractive; saat bermain natural number game, proof terasa hanya seperti daftar perintah rw [x] sehingga sangat sulit dibaca; memang editor bisa menunjukkan state tiap baris, tetapi harus terus klik dan itu merusak alur; kalau Python juga tanpa indentasi dan kita harus klik hanya untuk memahami struktur bloknya, rasanya akan sama; mungkin sudut pandang saya dipengaruhi keterbatasan perintah di awal game, tetapi saya penasaran apakah dalam lingkungan Lean penuh, alur ini terasa lebih baik

  • Apakah ada cara membaca bukti di Lean secara noninteractive?
    Saya juga baru-baru ini penasaran lalu mencarinya; blog lean-in-latex memberi cara untuk mengikuti alurnya di luar editor tanpa perlu klik, dan Anda juga bisa melihat bagaimana komunitas Lean mendekati hal ini

  • Di Rocq dulu pernah ada sesuatu yang disebut “bahasa pembuktian matematis”; sulit menemukan contoh penggunaan nyatanya, tetapi kira-kira seperti ini

    Lemma foo:
      forall b: bool, b = true -> (if b then 0 else 1) = 0.
    proof.
      let b : bool.
      per cases on b.
        suppose it is true. thus thesis.
        suppose it is false. thus thesis.
      end cases.
    end proof.
    Qed.
    

    Pendekatan ini membuatnya terbaca seperti “bukti tulis tangan” dalam makalah, tetapi hampir tidak dipakai sehingga menghilang; bahasa pembuktian Isar milik Isabelle juga mirip, bahkan lebih dekat ke cara standar; contohnya:

    lemma "map f xs = map f ys ==> length xs = length ys"
    proof (induct ys arbitrary: xs)
      case Nil thus ?case by simp
    next
      case (Cons y ys) note Asm = Cons
      show ?case
      proof (cases xs)
        case Nil
        hence False using Asm(2) by simp
        thus ?thesis ..
      next
        case (Cons x xs’)
        with Asm(2) have "map f xs’ = map f ys" by simp
        from Asm(1)[OF this] ‘xs = x#xs’‘ show ?thesis by simp
      qed
    qed
    

    Keseluruhan struktur logika dan hasil-hasil antara ditulis dengan jelas, lalu hanya pada bagian yang detailnya penting kita menyingkat tactic dengan “by ...”; saya tidak tahu apakah Lean punya hal seperti ini, tetapi setidaknya ini bisa jadi kata kunci pencarian atau bahan pertanyaan di forum Lean
  • Pertanyaan yang sangat bagus! Saya masih pemula jadi jangan dipercaya sepenuhnya, tetapi saya akan berbagi kesan saya; setelah sekitar dua bulan memakai Lean, membaca kode bukti terasa berbeda dari membaca kode program, lebih seperti “memindai”; saya jadi memperhatikan struktur argumen secara umum, tactic apa yang dipakai, dan lemma apa yang dipakai; gaya kode Lean yang nyata biasanya menambah indentasi saat goal baru muncul, lalu menguranginya lagi saat goal selesai, jadi bentuk (“shape”) argumen penting saat membaca; lihat contoh PR saya; ketika sudah terbiasa dengan tactic, Anda akan mengenali bahwa intro berarti masuk ke quantifier, constructor berarti membagi goal, dan seterusnya; pada akhirnya tactics adalah makro/DSL yang membentuk pohon bukti (term tree), dan ketika saya melihat kode bukti rasanya seperti manipulasi pohon (memecah bagian, mengisi urutan, dan sebagainya); meski begitu, kebutuhan untuk klik tetap ada jika kita ingin tahu assertion tepatnya di tengah kode bukti; bukti yang idenya bagus bisa dibaca dengan jelas seperti alur logika dalam makalah, jadi orang yang ingin menyampaikan niatnya biasanya akan menulis nama yang mudah dibaca, alur yang jelas, mengekstrak lemma kecil, lalu menaruh hipotesis lebih dulu dan menyelesaikannya dengan kode bukti yang singkat; sebaliknya, bagian yang secara mekanis merepotkan tetapi jelas bagi matematikawan sering diperlakukan dengan “golfing” (menulis sesingkat mungkin); gaya golf sering memendekkan kode tetapi hanya menyentuh bagian yang sudah intuitif bagi manusia; singkatnya, struktur pembacaan di Lean memang implisit, tetapi ada cara untuk membuatnya lebih jelas, dan semakin mahir dengan tactic, semakin mudah memahami struktur tanpa klik; bahkan hanya dengan memindai nama lemma, Anda bisa menangkap alur besarnya, dan urutannya mudah direkonstruksi
• Isinya benar-benar bagus; saya rasa tidak banyak orang yang bisa menjelaskan hal seperti ini dengan cara yang mudah dicerna; rahasianya adalah memperlihatkan semua langkah kecil yang biasanya dilewati begitu saja oleh para ahli
  • Terima kasih!
• Saya penasaran apakah di thread ini ada pendapat tentang masa depan Lean vs idris/coq/agda; saya ingin mempelajari knowledge representation, tetapi sebelum mendalami salah satu, saya khawatir soal ukuran komunitas dan risiko masa depan; dulu saya pernah menginvestasikan waktu ke clojure core.logic lalu kapok karena minimnya minat dan kecilnya komunitas, jadi sekarang sulit memulai dengan santai
  • Dari pengalaman nyata saya, Lean dan Coq/Rocq dipakai jauh lebih banyak daripada Idris dan Agda, dan library serta komunitasnya juga terasa lebih besar; Rocq banyak dipakai untuk verifikasi program, yang menurut saya karena sejarahnya lebih panjang, meski ia juga punya banyak kekhasan sehingga Lean mungkin akan segera mengejar; Lean paling umum dipakai untuk pembuktian teorema matematika; proyek terkenal Rocq antara lain CompCert, CertiCoq, sel4, dan ada juga kasus pemakaian untuk verifikasi perangkat lunak pesawat sungguhan (lihat daftar proyek yang dirangkum), sementara di Lean ada mathlib (kumpulan bukti matematika), Teorema Terakhir Fermat (proyek pembuktian FLT), PFR, dan proyek besar lainnya; setahu saya Idris dan Agda tidak punya banyak proyek “dunia nyata”, walau saya bisa saja salah; semuanya tetap sangat kecil skalanya dibanding bahasa atau komunitas seperti C++ atau JavaScript, dan verifikasi program dalam praktik memang pekerjaan yang sangat lambat dan membosankan; mungkin suatu hari akan ada perubahan mendasar berkat kemajuan AI dan semacamnya, tetapi keterampilan yang dipelajari tetap akan berguna
  • Saya rasa sebenarnya tidak tepat “bertaruh” di bidang ini; kebanyakan matematikawan memang tidak terlalu tertarik pada formalization (formalisasi), karena jurang antara bukti tulisan tangan dan sintaks ketat yang diminta komputer terlalu besar; lebih baik mendekatinya sebagai sesuatu yang menyenangkan untuk dipelajari dan dipraktikkan; soal prospek masa depan, Lean memang belakangan tampak paling aktif, tetapi masing-masing punya basis pengguna lama, jadi sulit membuat prediksi pasti
• Saya penasaran apakah, tanpa teknik atau trik apa pun, kita bisa begitu saja melempar sesuatu secara acak ke Lean lalu mendapatkan temuan menarik berdasarkan apakah Lean meloloskannya atau tidak; atau apakah ini bisa dijalankan lewat sistem otomatis atau llm agar mencoba semua bukti/teori yang rumit lalu melihat apakah berhasil? Mungkin pertanyaannya terdengar aneh, tetapi saya bahkan baru sekadar memahami Prolog
  • Dari sudut pandang saya yang bekerja profesional di certified programming, saya rasa AI generatif dan metode formal adalah pasangan yang paling cocok; apakah nanti LLM akan menggantikan programmer atau tidak juga menurut saya bergantung pada seberapa baik AI menangani certified programming dan penalaran kombinatorial,

    Kalau dilempar acak, apakah bisa muncul temuan menarik?
    AI lama cukup baik pada masalah seperti checkers yang jumlah kemungkinannya kecil; catur sedikit lebih sulit, dan Go nyaris mustahil bagi AI nontradisional tanpa machine learning; bahasa formal punya jumlah kemungkinan dan state yang bisa dieksplorasi dalam skala yang hampir tak terbayangkan; kalau sifat masalahnya jelas, brute force dengan SMT solver memungkinkan; SMT solver dan proof assistant awalnya cabang metode formal yang berbeda, tetapi sekarang justru saling melengkapi (lihat Sledgehammer, Lean-SMT)
    Bagaimana kalau LLM atau sistem otomatis diminta mencoba bukti/teori sebarang?
    Ini memang belum jadi riset arus utama, tetapi banyak penelitian ke arah ini sudah dilakukan; bahkan sebelum ledakan LLM, sudah ada pendanaan besar selama bertahun-tahun; ada upaya lama seperti “Learning to Find Proofs and Theorems by Learning to Refine Search Strategies”, dan riset baru seperti DeepSeek-Prover; bagaimana tepatnya model-model ini dilatih dan sejauh mana kemungkinan masa depannya masih sangat terbuka,
    LLM saat ini masih kurang matang dalam bahasa Rocq dan Lean, dan begitu jawaban yang salah muncul, memperbaikinya sangat menyakitkan; namun saya tetap berharap kualitas tool AI akan meningkat besar seiring waktu

  • Ini benar-benar bidang riset dan eksperimen yang sangat aktif!
    Komunitas Lean banyak berkumpul di Zulip, dan Anda bisa melihat berbagai thread referensi di channel Machine-Learning-for-Theorem-Proving
• Sebagai orang yang pertama tertarik pada Lean setelah melihat alphaproof, tulisan pengantarnya sangat bagus; bolehkah saya tahu Anda sedang melakukan apa di Lean?
  • Untuk saat ini saya cuma belajar matematika dengan Lean; tepatnya mengikuti buku ajar Lean karya Tao, lalu mengisi bagian sorry yang masih kosong di latihan-latihannya sendiri (jawaban saya ada di sini)
• Saya penasaran apakah Lean punya mode verifikasi yang secara otomatis mencegah penggunaan hal yang tidak tepercaya (proof dengan sorry) atau penambahan aksioma ekstra, misalnya untuk memeriksa bahwa “proof sama sekali tidak memakai sorry dengan cara apa pun” dan “hanya bergantung pada kekuatan pembuktian dari himpunan aksioma yang tetap”
  • Saya rasa #print axioms some_theorem yang disebut di bagian akhir artikel mungkin contoh yang relevan; dengan itu kita bisa tahu apakah bukti tersebut secara langsung atau tidak langsung bergantung pada sorry atau aksioma yang belum ditinjau
  • Anda bisa memeriksa tidak adanya aksioma tambahan dengan print axioms, dan juga melihat apakah kompilasi berjalan tanpa warning atau error; utilitas SafeVerify juga menangkap beberapa trik yang ditemukan sistem RL
  • Ada juga penjelasan bahwa ini bisa dilakukan lewat macro di sini